Deductive databases, constraint satisfaction, Prolog, and formal verification are often defined as special cases of first-order logic. Here we define their simplest incarnations from the perspective of Herbrand logic, where the resulting definitions are identical to those usually given in for example Ullman's Database and Knowledge-base Systems or Lloyd's Foundations of Logic Programming book. Because Herbrand semantics is simpler to teach and understand than first-order logic, we hope our introduction to the foundations of these three applications are more accessible than the first-order introduction to those not familiar with logic.

Bilevel Reasoning

All four applications of Herbrand logic can be defined in a common framework: Bilevel Reasoning (BR). Bilevel reasoning focuses on reasoning about a pair <Γ, M>, where M is a model and Γ is a set of axioms. Γ conservatively extends the model M. The idea is that the model M picks out one world in the vocabulary V and the axioms Γ extend the theory defined by M to some theory in vocabulary V', which is larger than V.

Definition (Bilevel Pair): A bilevel pair is <Γ, M>, where M is a Herbrand model, Γ is a set of axioms, and vocabulary[Γ]∪vocabulary[M] is a vocabulary, denoted vocabulary[<Γ,M>].

Satisfaction for bilevel pairs can be defined using the notion of a model's reduct, which is just a way of talking about the portion of a model in a shrunken vocabulary.

Definition (Reduct): The reduct of model M wrt vocabulary V, written Reduct[M,V] is the intersection of M and the ground atoms of V.

Definition (Bilevel Satisfaction): Let <Γ, M> be a bilevel pair, where Γ consists of closed sentences. Let N be a model in the vocabulary V = vocabulary[Γ] ∪ vocabulary[M]. N satisfies the pair exactly when N satisfies Γ wrt V and the portion of N corresponding to the vocabulary of M is the same as M.

Just as the set of models for an axiomatization Δ is usually denoted Mod[Δ], we can use Mod[<Γ,M>] to denote the set of models that satisfy the bilevel pair <Γ,M>. Entailment in bilevel reasoning can therefore be defined follows.

Definition (Bilevel Entailment): Let P be a bilevel pair and φ a closed sentence. P entails φ exactly when every model that satisfies P satisfies φ.

This splitting of axioms and data is convenient, but often it is equivalent to a normal set of sentences in Herbrand logic.

Theorem (Finite Bilevel Equivalent to Herbrand Logic): Let <Γ,M> be a bilevel pair, where M is finite. Then there is a sentence set Δ in Herbrand logic such that Mod[Δ] = Mod[<Γ,M>].
Proof: First we construct such a Δ and then we show that every model that satisfies the pair satisfies it and vice versa.

Start out by including in Δ every sentence in Γ. Then for each relation r in M, perform the following. Let {t₁,...,t_n} be the set of ground tuples for which r is satisfied in M. Note this is a finite set. Include the sentence, ∀xbar.r(xbar) ⇔ xbar=t₁ ∨ xbar=t₂ ∨ ... ∨ xbar=t_n.

To show: |=_N <Γ,M> if and only if |=_N Δ. Since Γ is included in Δ, we can remove it from both sides. Using the definition of bilevel pair satisfaction, we need now show that M = Reduct[N,vocab[M]] if and only if |=_N ∀xbar. r_i(xbar) ⇔ xbar=t₁ ∨ xbar=t₂ ∨ ... ∨ xbar=t_n for all relations r_i in vocab[M].

(⇒) Suppose M = Reduct[N,vocab[M]] but for the purpose of contradiction there is some r_i such that |#_N ∀xbar. r_i(xbar) ⇔ xbar=t₁ ∨ xbar=t₂ ∨ ... ∨ xbar=t_n. That is, there is some tbar such that |#_N r_i(tbar) ⇔ tbar=t₁ ∨ tbar=t₂ ∨ ... ∨ tbar=t_n. That is, there is either some tbar in r_i in the reduct that is not in {t₁,...,t_n} or there is some tbar not in r_i in the reduct but in {t₁,...,t_n}. But in both cases, because the reduct of N is M, and {t₁,...,t_n} was constructed to be exactly that set of ground terms in r_i in M, neither of these can be the case. Contradiction.

(⇐) Suppose N satisfies ∀xbar. r_i(xbar) ⇔ xbar=t₁ ∨ xbar=t₂ ∨ ... ∨ xbar=t_n for all relations r_i in vocab[M], but for the purpose of contradiction M \ne Reduct[N,vocab[M]]. That is there is some r(ubar) extra in N or missing in N. Suppose the former, that r(ubar) is in Reduct[N,vocab[M]] but not M, i.e. ubar is not in {t₁,...,t_n}. Then N could not satisfy ∀xbar. r(xbar) ⇔ xbar=t₁ ∨ xbar=t₂ ∨ ... ∨ xbar=t_n since ubar is none of the t_i. Likewise, if r(ubar) is in M but missing from Reduct[N,vocab[M]] then again N cannot satisfy ∀xbar. r(xbar) ⇔ xbar=t₁ ∨ xbar=t₂ ∨ ... ∨ xbar=t_n since this sentence entails r(ubar). Contradiction. ∎

Clearly then every finite bilevel pair can be encoded as a finite set of Herbrand logic sentences. However, as we shall see, deductive databases and to a lesser extent formal verification take advantage of this separation. They along with CSPs and logic programming can be defined as subsets of a very special class of bilevel pairs--those with exactly one satisfying model.

In first-order logic, a set of axioms whose models are all elementarily equivalent, i.e. indistinguishable wrt first-order sentences, is said to be axiomatically complete. This means every sentence in the language or its negation is entailed by the axioms.

Definition (Axiomatic Completeness): Let L be a language and Δ a set of sentences. Δ is axiomatically complete if and only if for every closed sentence s in L, Δ entails s or Δ entails ¬s or both.

In Herbrand logic, if a set of sentences is axiomatically complete, those sentences are satisfied by exactly one model. (The fact that axiomatic completeness in Herbrand logic has different model-theoretic properties than first-order logic stems from the fact that Herbrand logic fixes the equality relation, whereas first-order logic does not.) Likewise, we will say that a bilevel pair is (axiomatically) complete if and only if it has a single model.

Definition (Complete Bilevel Pair): A bilevel pair P is complete if and only if Mod[P] is either a singleton set or the empty set.

Definition (Complete Bilevel Axioms): A set of bilevel axioms Γ is complete wrt vocabulary V if and only if for every model M in V such that P=<Γ,M> is satisfiable, P is a complete bilevel pair.

It is sometimes natural to think of Γ as simply extending the theory defined by M, a small wrinkle on the notion of a conservative extension to a logical theory.

Definition (Conservative Pair): A pair P=<Γ,M> is conservative exactly when every sentence in Cn[P] that is in vocabulary[M] is a consequence of M itself, i.e. when it is in Th[M].

Definition (Conservative Bilevel Axioms): A set of axioms Γ is conservative wrt vocabulary V if and only if for every model M in V, <Γ,M> is a conservative pair.

Deductive databases, constraint satisfaction, logic programming, and formal verification can all be defined as complete bilevel pairs.

A database is complete bilevel pair where the model that satisfies the pair is finite. Two standard options exist for defining the set of object constants in the vocabulary: (1) it consists of those object constants that appear in P or (2) it is the set of all object constants, i.e. it includes infinitely many object constants. We will assume the former: that the set of object constants is just those that appear in P.

Let <Γ,M> be a database. Using the conventional database terminology, the set of relations defined in M is the set of extensional database predicates (EDBs), i.e. the base tables, and the remaining relations comprise the set of intensional database predicates (IDBs), i.e. the views. When there are no IDBs, a database is just a Herbrand model, and there is always at least one EDB in every database.

A database query always takes the following form: find all the x₁,...,x_n such that the database satisfies the query φ(x₁,...,x_n). Various languages exist for expressing that query; here we discuss Datalog with negation, which is often used to define IDBs. Because a database is a complete pair, Datalog has been designed so that the negative consequences need not be written down (just like in a Herbrand model) but at the same time every set of Datalog rules can always be assigned a unique model. This turns out to be a little tricky with negation. As we shall see, this allows us to define a database as a bilevel pair in a fairly straightforward way: the model is the set of EDB predicates and the axiom set defines the IDB predicates with Datalog. The rest of this section defines Datalog with negation and discusses how to ensure a set of Datalog rules can be assigned a unique model.

Definition (Datalog Rule): A Datalog rule is an implication (where traditionally :- is used instead of ⇐ and , is used in place of ∧).

h ⇐ b₁ ∧ b₂ ∧ ... ∧ b_n
- The head, h, is an atomic sentence.
- Each element in the body, b_i, is a literal.
- There are no function constants.
- Safety: if a variable appears in the head or in a negative literal, it must appear in a positive literal in the body.

(Usually, Datalog allows various arithmetic operations in the body of rules, e.g. addition and multiplication, but we ignore those operations here. Also, the above definition is usually called datalog^¬.)

Datalog is usually viewed as a language for defining a larger database from a smaller one. It defines the contents of new relations based on the contents of the original relations, in the end producing a single model/database. Because Herbrand semantics allows multiple models to satisfy a particular set of sentences, as stated it is inappropriate for defining the semantics of Datalog rules. Three variations on Herbrand semantics are often used as the semantics for Datalog: minimal Herbrand semantics with stratified negation, stable model semantics, and well-founded semantics. We leave discussion of stable model semantics to the section on Prolog; well-founded semantics relies on 3-valued logic, which we do not address.

If a set of Datalog rules has no negation, i.e. when every literal in the body of every rule is an atom, it is Horn. It is well-known that Horn rules have a well-defined minimal model (as measured by the number of ground atoms in the Herbrand model), and the semantics for such a set of rules is defined to be that model. When the rules do include negation, the minimal model is not necessarily well-defined. For example, the sentence

p(a) ⇐ not q(a)

p(a) ∨ q(a)

While negation does present some problems for the notion of a minimal Herbrand semantics, certain forms of negation do have well-defined minimal models. Stratification is one such form. It is defined in terms of a dependency graph.

Definition (Dependency graph): Let Δ be a set of Datalog rules. The nodes of the dependency graph for Δ are the relation constants in the vocabulary. There is an edge from r₂ to r₁ whenever there is a rule with r₁ in the head and r₂ in the body. That edge is labeled with ¬ whenever r₂ is in a negative literal.

Definition (Datalog Stratification): A set of Datalog rules are stratified when its dependency graph contains no cycle through a negative edge. Stratum 0 is the set of all nodes without incoming edges. Stratum 1 is the set of all nodes adjacent to a node in stratum 0; stratum i+1 is the set of all nodes adjacent to a node in stratum i that are not in stratum i.

Clearly, if there is no negation, the graph has no ¬ edges, which means it has a single stratum and is stratified. When a set of Datalog rules is stratified, we can always choose a single Herbrand model as its semantics. Stratum 0 contains no negation; thus it has a minimal model. The minimal model for stratum i+1 is constructed by extending the minimal model for stratum i by evaluating the body of all rules in stratum i+1 in the minimal model of stratum i.

Definition (Stratified Datalog Semantics): Let S be a set of stratified Datalog rules. Let M₀ be the minimal models that satisfies all the rules in stratum 0. To compute M_i, where i > 0, initialize M_i to M_i-1. Perform the following operations, adding the result to M_i until no changes occur.

• Let h ⇐ b₁ ∧ ... ∧ b_n be a rule in stratum i.
• For each substitution σ such that |=_Mi (b₁∧ ... ∧ b_n)σ, output hσ.

For example, consider the following stratified rules. (Traditionall not is used in place of ¬.)

p(a) ⇐ ¬q(a)
q(b) ⇐ not t(b)
t(c)

{t(c)}.

{t(c), q(b)}.

{t(c), q(b), p(a)} ∎

Variables in negative literals can be problematic. Consider the rule set

p(x) ⇐ ¬q(x)
q(a)

The definition for a Datalog rule includes a statement that says for an implication to be a Datalog rule, it must obey the following constraint: if a variable appears in the head of the rule or a variable appears in a negative literal, that variable must also appear in a positive literal in the body. Now that the semantics have been defined, the reason for this constraint can be explained.

Suppose we were to write a rule with a variable in the head that does not occur in the body or a rule with a variable in a negative literal that does not occur in the body.

p(x,y) ⇐ q(x)

s(a) ⇐ ¬ r(y)

In the second rule above, it is unclear how to interpret what the rule is supposed tomean. Does it mean that if there is some y for which r is false that s(a) is true? Or does it mean that if r(t) for every ground term t is false that s(a) is true? the constraint on Datalog rules removes this ambiguity by requiring every variable in a negative literal to also occur in a positive literal in the body; by first evaluating the poositive literal, every negative literal can be ground before evaluating it using negation as failure.

Now that the syntax and semantics of Datalog have been covered, we can return to the earlier promise of defining a database in terms of a bilevel pair.

Observation (Database as a Bilevel pair): A database is a bilevel pair <Γ,M>, where Γ is a finite set of Datalog rules that has no EDB predicate in the head of any rule.

We now turn to some decidability results. Because Datalog does not allow function constants, the number of Herbrand models for any finite vocabulary is finite. Regardless which semantics are used, as long as the semantics assigns some subset of all Herbrand models over a finite vocabulary to a set of sentences and checking satisfaction in one of those models is decidable, entailment is decidable.

Theorem (Datalog is Decidable): Let Δ be a finite set of Datalog rules. Let S be a semantics for Datalog that chooses some subset of the Herbrand models over the vocabulary induced by Δ, where checking whether a model satisfies Δ is decidable. Let φ be the query.

Unlike theorem proving, answering a query in a database usually means finding all the tuples for which the query is satisfied. We call this materializing the query.

Definition (Materialization): Let Δ be a set of sentences and φ(x₁,...,x_n) be a query with free variables x₁,...,x_n. The materialization of the query for Δ is the set of all <t₁,...,t_n> such that Δ |= φ(t₁,...,t_n), where each t_i is ground.

Corollary (Materializing Datalog is Decidable): Same conditions as the last theorem. φ has the free variables x₁,...,x_n. Materializing φ for Δ is decidable.
Proof: Let σ be some substitution x₁/c₁,...,x_n/c_n, where each c_i is an object constant in the vocabulary of Δ. By the above theorem Δ |= φσ is decidable. If Δ |= φσ, add the tuple <c₁,...,c_n> into the materialization. Since φ is finite, the number of variables is finite; since Δ is finite, the number of object constants is finite. Thus, the number of distinct σs is finite; check entailment for each one and return the resulting set of tuples. ∎

Completeness and NAF implementation

When a theory in a complete logic, i.e. a logic with a complete proof procedure, is axiomatically complete and has a recursively enumerable axiomatization, the theory is decidable: for any query φ, interleave proof attempts for φ and ¬ φ. One of them is entailed, and because the logic is complete, the proof will be found. In such a theory, negation as failure (NAF) is monotonic: failing to prove φ ensures that ¬ φ is entailed.

Definition (Negation as Failure): Negation as failure is the following inference rule:

NAF is monotonic whenever Δ entails either the query in question or its negation, i.e. Δ is complete for the language that includes either the query or its negation.

Theorem (Monotonic NAF): NAF is monotonic for a particular query φ if and only if the theory is complete wrt the language {φ}.
Proof:

Δ |= φ ∨ Δ |= ¬φ (Δ is complete)
⇔ ¬ (Δ |= φ) ⇒ Δ |= ¬φ (Logical equivalence of p ∨ q and ¬ p ⇒ q)
⇔ Δ |# φ ⇒ Δ |= ¬φ (Every query is either entailed or not entailed)∎

Because the Stratified Datalog semantics assigns a single model to a set of rules, it ensures every theory is axiomatically complete. The above theorem ensures NAF is monotonic for every query. One benefit to these semantics is that there need be no rules with negative literals in the head, which is reflected in the definition of Datalog rules.

Since the negative portion of the theory is never explicitly written, a proof system for Datalog must rely on NAF. The definition of Stratified Semantics can be implemented directly, causing the proof system to construct the minimal model by constructing one stratum after another in a bottom-up fashion. Some implementations, on the other hand, start with the query and use the rules backwards. They evaluate negative literals in rule bodies with NAF: attempt to prove the positive version of the literal, and if that fails, conclude that the negative version must be true. If done naively, the proof procedure can fail to find a proof even when one exists.

For example, consider the following rule-set.

p(x,y) ⇐ p(x,z) ∧ p(z,y)
q(a) ⇐ not p(a,a)
q(a)

q(a) is true if p(a,a) cannot be proven
p(a,a) can be proven if p(a,z) and p(z,a) can be proven
p(a,z) can be proven if p(a,w) and p(w,z) can be proven
...

This example illustrates a fundamental feature of the top-down approach: while answering a Datalog query is decidable, the naive top-down approach does not always decide it whereas the naive bottom-up approach will. For example, the query p(a,a) may run forever. Moreover, it is hard to make the top-down approach decide such queries efficiently, even with sophisticated methods.

Finite constraint satisfaction problems turn out to be a subclass of database queries. Infinite constraint satisfaction problems would also fall into a subclass of database queries if databases were allowed to be infinitely large. However, instead of finding all solutions to the query as is done in databases, a constraint satisfaction problem is solved once any one solution is found.

Definition (Constraint Satisfaction Problem): A constraint satisfaction problem is a three-tuple <V,D_V,C_V>:

V: set of variables
D_V: for each variable, a set of values, i.e. its domain
C_V: a set of constraints that say which combinations of variables can be assigned which combinations of values

Mathematically, the constraints in a CSP can be defined as tables of the allowed values. For example if variables v₁ and v₂ have the same domain {a,b,c} but some constraint says those variables can only be assigned different values, that constraint is mathematically equivalent to the following table.

A set of constraints is then a set of tables, where each column is labeled with a variable name. In the context of databases, these tables labeled C_i is correspond to the EDBs. In logic, we encode the table for constraint C_i as the set of all ground atoms of the form C_i(t₁,...,t_n), where n is the number of columns and t₁,...,t_n is some tuple in the table. The CSP is solved by a variable assignment that satisfies all the constraints. The set of all such variable assignments is defined by the following conjunction. For each table C_i with columns labeled v₁,...,v_m, include the conjunct C_i(v₁,...,v_m). This is a special kind of database query--a conjunctive query or equivalently a select-project-join query. Or equivalently, the query is just the natural join on all the tables.

For example, suppose there were two of the tables as shown above: C₁ and C₂, the first labeled the same as above, v₁ on the left and v₂ on the right, and the second labeled differently, v₂ on the left and v₃ on the right. The constraint satisfaction problem would be asking for an assignment v₁/t₁, v₂/t₂, and v₃/t₃ so that <t₁,t₂> is a tuple in the C₁ table and <t₂,t₃> is a tuple in the C₂ table. The corresponding conjunctive query would be C₁(v₁,v₂) ∧ C₂(v₂,v₃). All solutions to that query over those tables is the following, which is equivalent to the natural join of C₁ and C₂.

The constraints in a CSP are often stated more compactly, in Datalog. At first, this equivalence of CSPs with a subset of databases is disconcerting since solving a CSP is well-known to be NP-Complete and answering queries in databases is often considered to be polynomial. To rectify this seeming contradiction, it is sufficient to note that solving a CSP is NP-hard in terms of the number of variables. Solving a database query is polynomial in terms of the data, i.e. in terms of the size of the model; it is exponential in the number of variables in the query. Thus, database queries are in practice usually polynomial because the size of the data vastly exceeds the size of the query--the major cost in answering a database query is in manipulating the data. Not independently, the number of answers to a query is often much larger than the number of variables in the problem, which gives further support for ignoring the number of variables, as is often done in the database community.

Observation (CSP as a Bilevel pair): In the context of bilevel reasoning, a CSP is a bilevel pair <Γ,M>, where Γ is empty, and the only query of interest is the natural join over all the relations in M (if we gave names to each argument of each relation).

This section is entitled Logic Programming, though with some apprehension. Truly this section is about Prolog and variants of it--a family of languages that were developed to program computers where all the logic is in rule form, and negation as failure is prevalent. Logic programming on the other hand is the far more general paradigm of programming a computer using formal logic itself, regardless the syntax or semantics. It is noteworthy that Prolog and its variants have become so popular that they have become synonymous with the term logic programming.

Prolog can be seen as a generalization of Datalog, and in the context of Bilevel reasoning, it is a complete bilevel pair <Γ,M>, where M can be empty. Function constants come into the picture, certain restrictions are removed, and a more general rule form is often allowed. The Declarative Logic Program (see, for example Alsac and Baral's comparison of DLP and Description logic) is one of the most general forms of logic programming.

Definition (Declarative Logic Program Rule): A Declarative Logic Program rule is an implication (where traditionally :- is used instead of ⇐ and , is used in place of ∧).

h₁ ∨ ... ∨ h_m ⇐ b₁ ∧ b₂ ∧ ... ∧ b_k, not b_k+1 ∧ ... ∧ not b_n
- each h_i is a classical literal, e.g. p(a) or ¬p(a).
- each b_i is a classical literal.
- each not b_j is a NAF literal, e.g. not p(a) or not ¬ p(a) ∎

When compared to the definition of a Datalog Rule, (1) disjunction is allowed in the head, (2) classical negation is allowed everywhere , (3) variables are unrestricted, and (4) function constants are allowed. The most widely-used form of logic programming, Prolog, does not allow (1) or (2). It is this version of logic programming we assume from this point on, making the definition as follows.

Definition (Prolog): A Prolog is an implication.

h ⇐ b₁ ∧ b₂ ∧ ... ∧ b_n
- h is an atom.
- each b_i is a NAF literal, e.g. p(a) or not p(a). ∎

Just as with Datalog, a set of Prolog sentences without negation can be assigned a single, minimal model; that model happens to be the intersection of all the Herbrand models of those sentences. Negation presents difficulties in Prolog just like it did with Datalog.

The Stratified Datalog semantics works equally well with function constants, but researchers have found stratification sometimes too restrictive; two definitions for the semantics of Prolog rules with negation stand out. [Gelfond and Lifschitz 1988] introduced Stable Model Semantics, and [Gelder, Ross, and Schlipf 1991] introduced Well-founded semantics. Stable model semantics are closer to Herbrand semantics than minimal Herbrand semantics: a Prolog theory under stable model semantics is not necessarily axiomatically complete, i.e. instead of assigning a single model to a set of sentences, it assigns multiple models. Well-founded semantics relies on a 3-valued logic, which in some sense compresses multiple models into a single one. Here we discuss only stable model semantics. These semantics do not naturally fit into the complete bilevel pair formalism, the stratified semantics do.

Propositional stable model semantics relies on the notion of a stable model, which in turn relies on the Gelfond-Lifschitz transformation.

Definition (Gelfond-Lifschitz Transformation): Let Δ be a set of ground Prolog rules and M a Herbrand model in the vocabulary of Δ. The Gelfond-Lifschitz transformation of Δ with respect to M is defined as follows.

1. Delete any rule in Δ with a literal not b_i in the body where b_i ∈ M.
2. Delete all negative literals from rules in Δ.

The result of this transformation with respect to a model M is a set of rules without negation. If M is minimal, it is a stable model.

Definition (Stable Model): Let Δ be a set of ground Prolog rules and M a Herbrand model in the vocabulary of Δ. M is a stable model of Δ if and only if M is the minimal satisfying model of GL[Δ,M].

There will always be exactly one minimal model of GL[Δ,M] since it is Horn.

Definition (Propositional Stable Model Semantics): Let Δ be a set of ground Prolog rules. Δ |= φ if and only if every stable model of P satisfies φ.

Definition (Stable Model Semantics): Let Δ be a set of Prolog rules. Let Δ' be all ground instantiations of the rules in Δ. Δ |= φ if and only if Δ' |= φ.

Regardless which semantics are chosen, a query in Prolog is a single atomic sentence. If the query φ = p(t₁,...,t_n) has variables, four options arise for answering the query: (1) return T if ∃*φ is entailed by the Prolog rules, (2) return some variable assignment σ such that the rules entail φ.σ, (3) return a function that iteratively returns such variable assignments, or (4) return all such variable assignments. Part of the reason (3) and (4) are not considered in Datalog is that every Datalog query has finitely many answers, whereas in Prolog there may be infinitely many answers.

Recall that answering entailment queries in Datalog is decidable, as is finding all answers to Datalog queries. The addition of functions ensures that undecidable problems can be embedded in Prolog, even without employing negation (see the comments about encoding Diophatine equations on Proof and Model Theory). That is, entailment queries for recursive Horn rules with functions is undecidable. Removing either functions or recursion regains decidability.

Theorem: Entailment for Horn Prolog is undecidable.

Theorem: Entailment for non-recursive Horn Prolog is decidable.

Theorem: Entailment for function-free Horn Prolog is decidable.

For more information on the semantics of Prolog and its variants, Lifschitz's paper entitled Foundations of Logic Programming surveys various semantic definitions and their computational consequences. It focuses on rules that include classical negation and on stable model semantics, closely connected to answer set programming.

Formal verification at a very high level involves defining how a system works and asking whether that system obeys some property. For example, given a computer program written in C, does it ever access an element of an array before allocating the memory for that array? Here we consider a very simple class of systems: finite state machines that run forever. While this class is simple, it should be noted that it is complex enough to model the workings of any modern-day computer.

First we show how to use a bilevel pair to define a system, and then we show how to phrase queries about that system.

Definition (Finite State Machine): A finite state machine (FSM) is a tuple <S, Σ, S₀, S_f, δ>. S: set of states Σ: input vocabulary S₀: the initial state -- S₀ ∈ S S_f: the final states -- S_f ∈ S δ: the transition function: SxΣ \rightarrow S. <∈dent>

It turns out to be convenient to use Vanilla Prolog with stratified semantics, i.e. Datalog with function constants, for encoding the FSM. Now we explain how to describe a finite state machine as a bilevel pair <Γ,M>.

Representing a FSM as a shown above may require a large amount of space; simply because the set of states may be very large. Often, though, the states in a system need not be described as monolithyic states but rather can be described using a set of propositions, where a state is defined as the set of propositions true in the state. Those propositions will be represented by ground terms.

The model M defines the propositions true in the initial state, S0. If for example the propositions p, q, and r are true in the intial state, and only those are true in the initial state, then the model is.

init(p)
init(q)
init(r)

The dynamics of most systems are the same regardless what the initial state is. Those dynamics (δ) tell us for a given state and a given input what the next state will be. To represent that proposition p is true in state s, we write

true(p,s)

To represent names for states, we will borrow from situation calculus. Each state may have many names; each name encodes the history of actions required to reach that state from the initial state. This reflects the fact that even though there are a finite set of states in a FSM, any one state may be reached arbitrarily many times by performing longer and longer sequences of actions from the initial state.

Thus, actions too take the form of propositions, and when encoded in logic the form of ground terms. If the proposition p is true in the state resulting from executing actions a,b,c from the initial state, we can express this as follows.

true(p, do(c, do(b, do(a, s0))))

To tie the initial state to the state name s0, we need a single rule.

true(x,s0) <= init(x)

Using simple implications, we can encode how certain actions affect the state of the world. Blocks world is a simple example. If blocks x and y are clear in state s (all of which are variables) then by executing the action stack(x,y) in s, the resulting state includes the proposition on(x,y).

true(on(x,y), do(stack(x,y),s)) ⇐ legal(stack(x,y), s)
legal(stack(x,y), s) ⇐ true(clear(x),s) true(clear(y),s)

Frame axioms, sentences that say what things do not change as a result of an action, must also be encoded. For example, if block x is on block y then performing the stack action does not change that fact. (Conditioning the rule on x and y being clear ensures the action is not executed unless it is legal to do so.

true(on(x,y), do(stack(z,w), s)) ⇐ true(on(x,y), s) legal(stack(x,y), s)

Datalog is useful here since it ensures that every proposition that cannot be proven true in a state is in fact false in that state, without having to write down all the rules that say so.

The set of all rules that define the transition function δ also define the input vocabulary Σ. Σ is the set of all ground action names. The remaining element of a FSM that must still be defined is the set of final states, Sf. To do that, we use a distinguished unary relation terminal. Whenever terminal holds in a state, the state is a terminal state, i.e. a member of Sf. For example, to say the system is terminal when block a is on b and block b is on c, we could write the following.

terminal(s) <= true(on(a,b),s) true(on(b,c),s)

To be faithful to the FSM notion of a terminal state, the rules for terminal should never distinguish states based on the state names, i.e. on the action taken to reach the current state. In other words, terminal(s) should always be at the head, and no action should ever be mentioned in the body.

The examples define a transition function as one would expect: given a state and an action, the rules say what the subsequent state looks like. But one could write more interesting rules where the state an arbitrary number of steps in the future determines what must have happened in the past.

true(p, s) <= true(p, do(a, do(b, s)))

Such rules can easily lead to inconsistency, and are never necessary for defining a finite state machine (though sometimes such rules are convenient). In the case that it is desirable to force a system description where the transition function is expressed only as the effects of an action on a current state, i.e. a Markov version of what is shown above, there is a language called GDL. It ensures decidability and finiteness, and can be easily translated into the form seen here.

Formal Verification Queries

For example, let's say we want to ask whether in every state reachable from the initial state the action a is legal.

First, we need to define which states are reachable. Again, we use Datalog to ensure we know which states are reachable and which states are not reachable.

reachable(s0)
reachable(do(x,s)) <= legal(x,s) reachable(s)

As. reachable(s) => legal(a,s)

Is there a legal move in each reachable state?

As. reachable(s) => Ea. legal(a,s)

Not every formal verification query can be phrased as a finite axiom about a bilevel pair. without extending the set of ground terms (and therefore the set of models. For example, does some property p hold over every subset of reachable states? Because the set of states can be arbitrarily large (depending on the model M), any relation of fixed arity will not be able to define any subset with more elements than the arity. Even if we were to extend the language with function constants to allow lists, the set of reachable state names could be countably large, which ensures the set of all subsets is uncountable. Clearly we cannot represent uncountably large sets in Herbrand logic since every model has only countably many elements. (Of course, if we were only interested in all the finite subsets of the reachable states, that set is still countable, and we could express it in Herbrand logic.)