Proving Semantic Properties as First-Order Satisfiability (Extended Abstract)

1 Introduction

Logic is often used to implement the expected functionality of databases (queries) or programs (executing them). In this setting, the following approach is naturally adopted [Green and Raphael, 1968]:

where Th is a logical theory representing the computational system and ϕ represents a computation.

Example 1 (Running example) Consider the following relational database about teachers a, b, c, d (of sort Teacher) and students p, q, r (of sort Student ) together with a relation teach giving information about the students taught by each teacher, according to the table [Reiter, 1977, page 59]

This table describes a (many-sorted) first-order theory Teach consisting of the following facts:

where teach is a binary predicate with arguments of sort Teacher and Student, respectively. A query asking for the students taught by teacher a would be encoded as:

McCune's (first-order) theorem prover Prover9 1 [McCune, 2005 2010] obtains a proof of (2).

Logic can also be used to prove properties of computational systems. For instance, knowledge stored in databases or computational properties of programs.

Example 2 The claim "every student is taught by some teacher" is expressed as follows:

Prover9 fails to prove (3). This is not surprising as (3) is not a logical consequence of Teach. Example 2 suggests that the logical-reasoning-as-logical-consequence approach (1) is "too strong" in some cases: our intuition that (3) should hold is not supported by (1).

As remarked by Clark, sentences expressing properties should be checked with respect to a given canonical model only [Clark, 1980, Chapter 4]. Similarly, in the logical approach to relational databases [Nicolas and Gallaire, 1977], solving queries and checking functional dependencies and integrity constraints is thought as the evaluation of logical formulas ϕ with respect to the facts stored in the database which are considered as a logical interpretation (or canonical, Herbrand model). Thus, we naturally consider the following:

where ITh represents such a canonical model. Note that ϕ in (4) does not need to be a theorem of Th (as in (1)); thus, we better generically call ϕ in (4) a semantic property of Th. As we prove in Example 14, (3) is a semantic property of Teach, thus recovering our intuition.

Thus, given a first-order theory Th, the following questions arise: (i) How to provide a generic notion of "canonical model" for Th? (ii) Accordingly, given a logical statement ϕ, what does it mean that ϕ "is a property" of Th? (iii) How to prove and disprove such properties? (iv) How to use the standard notions of provability and satisfiability for this purpose? (v) What kind of problems can be investigated in this way? Providing answers to these questions and related issues was one of the main goals of [Lucas, 2019] (although (i)-(v) are not explicitly formulated there). In the following, we provide answers to these questions.

1 http://www.cs.unm.edu/∼mccune/prover9/.

Along the paper, we use standard notions of many-sorted first order-logic (MS-FOL), see [Goguen and Meseguer, 1987; Hodges, 1993; Mendelson, 1997].

2 Semantic Properties of FOTheories

A natural candidate to play the role of canonical model for a theory Th is the set Th⊢ of ground atoms which can be proved from Th. Such a set of atoms can be seen as a Herbrand interpretation ITh: each function symbol f is interpreted as a mapping which, given a tuple t1, . . . , tk of ground terms returns a ground term f(t1, . . . , tk); each predicate symbol P is interpreted as the set of atoms P(t1, . . . , tn) in Th⊢ (more precisely, as the set of tuples (t1, . . . , tn) of ground terms such that P(t1, . . . , tn) ∈ Th⊢ ). This answers question (i) above: ITh is intended to be the canonical model for Th. In general, though, ITh may fail to be a model of Th [van Emden and Kowalski, 1976]: for Th = {p(a) ∨ p(b)}, we have Th⊢ = ∅; thus, ITh does not satisfy Th. However, for Horn theories 2 Th, ITh |= Th holds [van Emden and Kowalski, 1976]. Question (ii) is answered with the following definition.

Definition 3 (Semantic property) A formula ϕ is a semantic property of a theory Th iff ITh |= Th ∪ {ϕ}.

Remark 4 If ITh |= Th, then either ϕ or ¬ϕ is a semantic property of Th. If ITh |= ¬ϕ holds, then ITh |= ϕ does not hold and we say that ϕ is not a semantic property of Th. In contrast, there are theories Th and formulas ϕ where neither ϕ nor ¬ϕ can be proved in Th (which is often said to be an incomplete theory).

Regarding questions (iii) and (iv), for Horn theories Th, if ϕ can be proved from Th, then ϕ is a semantic property of Th. We can use any proof calculus (see [Fitting, 1996] for instance).

Remark 5 Theories usually specify true instances of relations only [Clark, 1977] and no negative information can be derived from them by logical reasoning. This means that using theorem proving to verify a semantic property ¬A for a given atom A is often hopeless.

We show that semantic properties ϕ of theories Th can be proved as satisfiability of an extended theory Th ∪ {ϕ} ∪ Zϕ where Zϕ is an auxiliary (possibly empty) theory which depends on the shape of ϕ only (see Corollary 13). For this purpose, we use the results in Section 3, based on the notion of preservation of logic formulas [Hodges, 1993].

2 A clause is a disjunction L1 ∨ · · · ∨ Ln of literals Li (which can be atoms Ai or negations of atoms ¬Ai). A Horn theory is a set of clauses each of them having at most one atom.

Examples of use. Finally, regarding question (v), computational systems that can benefit from our approach, involving the specification of clausal or even Horn theories, include Relational and Deductive Databases; Logic and Answer Set Programming; and Rewriting-Based Systems. See [Lucas, 2019, Section 4] and also Section 6 below.

In this section we have advanced some answers to questions (i)-(v) above. The next sections provide further details.

3 Preservation of MSFO Sentences

In the following, Th is a theory and we consider sentences ϕ in prenex form (5) as follows:

where (a) for all 1 ≤ i ≤ m and 1 ≤ j ≤ ni, Lij are literals Lij = Aij or Lij = ¬Aij for some atom Aij (in the first case, we say that (the sign of) Lij is positive; otherwise, it is negative [van Emden and Kowalski, 1976]) (b) x1, . . . , xk for some k ≥ 0 are the variables occurring in those literals (of sorts s1, . . . , sk, respectively), and (c) Q1, . . . ,Qk are universal/existential quantifiers. A sentence (5) is said to be positive if all literals are; if, additionally, Qq = ∃ for all 1 ≤ q ≤ k, then it is an Existentially Closed Boolean Combination of Atoms (ECBCA).

Theorem 6 Let A be a model 3 of Th, and ϕ as (5) be such that (a) for all q, 1 ≤ q ≤ k, if Qq = ∀ then hsq is surjective 4 and (b) for all negative literals ¬P(t1, . . . , tn) in ϕ and ground substitutions σ, if (h(σ(t1)), . . . , h(σ(tn))) ∈ P A then (σ(t1), . . . , σ(tn)) ∈ P ITh . If A |= ¬ϕ, then ITh |= ¬ϕ.

Remark 7 (Verification as satisfiability) We can verify whether ϕ is a semantic property of a Horn theory Th by satisfiability as follows: (i) let ϕ be ¬ϕ; then (ii) find a structure A satisfying (a) and (b) with regard to ϕ and such that (iii) A |= Th∪{ϕ} holds (note that ¬ϕ and ϕ coincide). By Theorem 6, ITh |= ϕ holds. Since ITh |= Th holds, ϕ is a semantic property of Th (Definition 3).

Models A required in Theorem 6 can be obtained from Th ∪ {ϕ} by using model generators like AGES 5 [Guti´errez and Lucas, 2019a] or Mace4 6 [McCune, 2005 2010].

Example 8 The question "is d teaching someone?" can be expressed as an ECBCA:

With AGES, we obtain a model of Teach ∪ {¬(6)}, i.e., of

3 A (many-sorted) structure A is an interpretation of sorts s as sets As (the carriers), function symbols f : s1 · · · sk → s as mappings f A : As1 × · · · ×Ask → As, and predicate symbols P as relations P A ⊆ As1 × · · · ×Asn . If A satisfies all formulas in a theory Th, we say that A is a model of Th.

4 A mapping f : A → B is surjective if for all b ∈ B there is a ∈ A such that f(a) = b.

5 http://zenon.dsic.upv.es/ages/

6 https://www.cs.unm.edu/∼mccune/prover9/

where AStudent = {-1, 0, 1} and ATeacher = N - {0}. For constants of sort Teacher, aA = bA = cA = 1, and dA = 6; for all constants of sort Student, pA = qA = rA = 1. Predicate teach is interpreted by teachA(x, y) ⇔ x ≤ 3. By Theorem 6, (6) is not a semantic property of Teach.

The treatment of condition (a) in Theorem 6 (surjectivity of hs for a given sort s) is considered in Section 4. Regarding condition (b) (if negative literals ¬P(t1, . . . , tn) are used in ϕ), given a predicate P : w where w = s1 · · · sn for sorts s1, . . . , sn, let NTh(P) = Iw - P ITh be the tuples (t1, . . . , tn) (of terms t1, . . . , tn of sorts s1, . . . , sn) which are obtained as the complement of the ) interpretation of P in ITh. Let NTh(P) = {¬P(t1, . . . , tn) | (t1, . . . , tn) ∈ NTh(P)} be these tuples viewed as negative literals.

Remark 9 In general, NTh(P) is infinite and incomputable. A finite description of NTh(P) can be given if the set TΣsi of terms of sort si is finite for all 1 ≤ i ≤ n.

Corollary 10 Let A be a model of Th ∪ NTh,ϕ such that for all q, 1 ≤ q ≤ k, if Qq = ∀ then hsq is surjective. If A |= ¬ϕ, then ITh |= ¬ϕ.

Example 11 According to Remark 7, we prove that (3) is a semantic property of Teach by first obtaining ¬(3), i.e.,

and then applying Corollary 10 with ϕ = (8). Since

we have to consider NTeach,¬(3) = NTeach(8), which is

The proof finishes in Example 14 below.

4 Surjective Homomorphisms

In Theorem 6 and Corollary 10, ensuring surjectivity of hs : TΣs →As is important to use them. We guarantee surjectivity of hs by satisfiability of an appropriate theory. Given a set T ⊆ TΣs of ground terms of sort s, let

Example 12 For T = {a, b, c, d} (containing all terms of sort Teacher), SuHTTeacher is

If A |= Th ∪ {SuHTs } holds, then hs is surjective. Expression SuHTs is first-order for finite sets T only. Moreover, not only the number but also the specific shape of terms in T can be important for SuHTs to work [Lucas, 2019, Remark 44]. Thus, a complementary approach is necessary, see [Lucas, 2019, Section 6.2] for details and examples. Overall, given a sentence ϕ, let Hϕ and Nϕ be appropriate (maybe empty) versions of SuH and NTh,ϕ as discussed above to be used with ϕ. We finally recast Corollary 10 as follows:

Corollary 13 (Satisfiability criterion) Let Th be a theory, ϕ be as (5), and A be a structure.

Example 14 For SuHTTeacher in Example 12 and NTeach,¬(3) in Example 11, a model A of

is obtained using Mace4 7 where ATeacher = AStudent = {0, 1, 2, 3}; aA = pA = 0, bA = qA = 1, cA = rA = 2, and dA = 3; finally teachA = {(0, 0), (0, 1), (1, 1), (2, 2)}. By Corollary 13, (3) is a semantic property of Teach, as expected.

5 RefutationWitnesses

A semantic value b such that ¬ϕA(b) holds is a counterexample to (∀x) ϕ(x). However, it is often desirable to provide terms t such that tA = b for a better understanding. Then, we say that ¬ϕ(t) is a refutation witness [Lucas, 2019, Definition 53]. In order to obtain them, consider the negation of (5), i.e.,

where Qi is ∀ whenever Qi is ∃, and ∃ whenever Qi is ∀.

Example 15 The claim "all students are taught by at least two teachers" is expressed as follows:

Below, we prove that (10) is not a semantic property of Teach and show a refutation witness. First, consider its negation

in the normalized format (5).

Model generators often transform sentences into universally quantified formulas by Skolemization (see, e.g., [Kim and Zhang, 1994]). If (9) contains existential quantifiers, we remove them by introducing appropriate Skolem function symbols sk : w → s where w is a (possibly empty) sequence of sorts. Thus, our satisfiability techniques would be applied to the Skolemized version (¬ϕ)sk of the negation of the target formula ϕ.

Example 16 The Skolem normal form of (11) is

where skz is a new Skolem constant of sort Student. Thus, (¬(10))sk is (12). According to Corollary 13, we would prove that (10) is not a semantic property of Teach by obtaining a model of Teach∪H(10)∪N(10)∪{¬(10)}. Using (12) instead of ¬(10), we rather seek a model of

7 For model generators, like Mace4, which do not support sorts, all sort information is removed before model generation, see (Sect. 5.2) for technical details.

Since universally quantified variables in (10) are of sort Student, H(10) = SuHTStudent for T = {p, q, r}. Since the only negative literal in (10) concerns the equality, we let

using x ̸= y instead of ¬(x = y), for short. A model A of (13) is obtained with AGES, where AStudent = {-1, 0, 1} and ATeacher = N ∪ {-1}. For constants of sort Teacher, aA = 0, bA = 1, cA = -1, and dA = 2; for constants of sort Student, pA = 0, qA = -1, and rA = 1. Also, sk Az = 1, and teachA(x, y) ⇔ x + y ≤ 0.

Constant skz in Example 16 represents the existential quantification in (11) (i.e., in (¬10)). Value sk Az = 1 represents the desired counterexample to (10). As discussed above, returning "1" is meaningless to the user, as it has to do with our proof-as-satisfiability approach. Returning "skz" is not helpful either, as symbol skz is not part of the original userdefined signature of the problem, being introduced during the model generation process. Our solution invoves the use of the inverse of hs for sorts s with Skolem symbols sk : w → s to retrieve a term of sort s with the same interpretation as sk . For this purpose, (i) surjectivity of hs is required (so that the existence of terms t of sort s such that hs(t) = sk A is guaranteed), and then (ii) we choose among terms t satisfying this condition. In this way, we obtain refutation witnesses built from symbols in the original signature only.

Example 17 For (10), since sk Ax = 1, the only term t ∈ TΣStudent such that tA = sk Ax = 1 is r. We obtain the following refutation witness:

which, in the following, maybe clearer, equivalent version

expresses that r is taught by a single teacher.

6 RelatedWork and Applications

In the following, we summarize some related work and applications concerning our approach.

Verification of concurrent systems. Lisitsa investigates reachability problems for transition systems represented as finite automata (with the possibility of using some arithmetic operators together with standard arithmetic properties encoded as equations) by using a logic-based approach similar to ours [Lisitsa, 2013]. Only monadic predicates are considered, though. Furthermore, only ECBCA sentences are used as semantic properties.

Protocol verification. Selinger shows how to encode cryptographic protocols as first-order formulas so that a proof of correctness of a given protocol can be pursued by just finding a model of a set of axioms representing properties of cryptographic properties together with a description of some particular protocol, and (the negation of) a formula Ψ which represents a violation of secrecy [Selinger, 2001]. GoubaultLarrecq shows that formally checkable proofs of correctness of protocols can be derived from the obtained models [Goubault-Larrecq, 2010]. He also investigates the specific interest (concerning decidability issues) of using finite models in protocol verification (he also shows that some protocols require infinite models). In these two papers, the considered formulas Ψ are ECBCAs. J¨urgens and Weber use a similar technique, where theories are restricted to limit sentences, which are universally quantified implications where some variables in the consequent can be quantified with the uniqueness quantifier ∃! instead [J¨urjens and Weber, 2009]. Sentences to be refuted (called conjectures) must be universally quantified conjunctions of atoms (∀⃗x) ∧ni=1 Ai. They consider finite models only, although no strong technical reason is apparently given to justify this restriction (which is not imposed in [Selinger, 2001], for instance).

Proof by consistency. The idea of proving logic formulas ϕ with respect to a theory Th by showing that Th ∪ {ϕ} is not contradictory is called proof by consistency in [Kapur and Musser, 1987]. The authors point that this proof method is, in general, unsound, but can be faithfully used with strongly complete proof systems, which are those guaranteeing that, whenever a formula ϕ can be added as an axiom to the proof system without introducing inconsistencies, then ϕ is also a theorem of the system. Kapur and Musser focus on manysorted equational proof systems consisting of a subset C of ground terms and a set of equations E where equational logic is used as proof system. Their proof by consistency method is used to prove equations (with implicit universal quantification) with respect to the considered systems. Furthermore, additional requirements like unambiguity are required on the considered systems (i.e., theories, see [Kapur and Musser, 1987, Theorem 9.2], for instance. Moreover, Kapur and Musser do not use satisfiability to show consistency of the theory (although both notions are equivalent) Instead, prooftheoretic (rewriting-based) methods are used to prove consistency.

Feasibility framework. The framework in [Guti´errez and Lucas, 2019b] has been recently extended to automatically prove and disprove ECBCAs (as feasibility goals). The system infChecker 8 provides a first implementation of the framework which has been shown successful in the infeasibility competition of the 2019 Confluence Competition [Middeldorp et al., 2019, Section 5.2] for Conditional Term Rewriting Systems. By infeasibility it is meant the absence of a substitution σ which makes a boolean combination ∨mi=1 ∧ni j=1 Aij of atoms Aij provable after instantiation with σ. As shown in [Lucas, 2020], infeasibility of first-order formulas is also useful in proofs of operational termination of programs in general logics [Meseguer, 1989].

8 http://zenon.dsic.upv.es/infChecker/