Evaluating Formulas in Finite Structures
Recall semantic function definitions for First-Order Logic Semantics.
Suppose , is a finite set and is given by explicitly listing their values for all argument tuples (e.g. in a table).
Then evaluation functions and give algorithms to determine the truth value of .
This is the model checking problem for first-order logic on finite structures: is a given interpretation model of .
Applications of Formula Evaluation
Uses of this algorithm: state of a software system is given as interpretation .
- database constraint integrity checking
- run-time checking
Example: Checking Database Integrity Constraint
Database integrity constraint:
ALL studentID. ALL courseID. Registered(studentID,courseID) --> (EX courseName. courseCatalog(courseID, courseName))
Example: Checking Assertion in Program with Heap
List contains no duplicates:
ALL n1. ALL n2. ListNode(n1) & ListNode(n2) & data(n1)=data(n2) --> n1=n2
Efficiency of Evaluating Formulas
Given a language , formula a formula in and an interpretation , determine .
Basic idea: to evaluate quantifiers, iterate over all domain elements.
- fix formula, change domain size : LOGSPACE (number of vars fixed, number of their bits changes)
- fix language with symbols of bounded arity, change formula: PSPACE (number of variables increases with formula size, see also QBF)
- Neil Immerman: Descriptive Complexity, Springer