LARA

Evaluating Formulas in Finite Structures

Recall semantic function definitions for First-Order Logic Semantics.

Suppose $I=(D,\alpha_I)$, $D$ is a finite set and $\alpha_I$ is given by explicitly listing their values for all argument tuples (e.g. in a table).

Then evaluation functions $e_F$ and $e_T$ give algorithms to determine the truth value of $F$.

This is the model checking problem for first-order logic on finite structures: is a given interpretation model of $F$.

Applications of Formula Evaluation

Uses of this algorithm: state of a software system is given as interpretation $I$.

  • 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 ${\cal L}$, formula a formula $F$ in ${\cal L}$ and an interpretation $I=(D,\alpha)$, determine $e_F(F)(I)$.

Basic idea: to evaluate quantifiers, iterate over all domain elements.

  • fix formula, change domain size $|D|$: 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)

References