LARA

This is an old revision of the document!

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$.

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

Example: Checking Assertion in Program with Heap

Example: Checking Program Designs

Efficiency of Evaluating Formulas

  • Neil Immerman: Descriptive Complexity