Interpretation Representation and Model Verification

Background

What is an Interpretation?

Why is Model Finding Useful?

• Checking the consistency of an axiomatization. [Sutcliffe]
• Finding the countermodel for a conjecture [Claessen], in particular ...
• In fault finding applications, e.g., in software verification, a countermodel for a proof obligation points to the location of the fault. [Sutcliffe]
• Finding a solution to a problem that is coded as a model finding problem. [Claessen]
• In teaching it is really useful to inspecting outcomes of student's experiments. [Steen]

1. Give only a "yes", indicating that there is a model.
   • In an (industrial) application where models indicate bugs, users would probably get very frustrated. [McCune]
   • Acceptable, but a model is preferred. [Claessen]
   • As part of a decision procedure, sat/unsat could be used as a yes/no subroutine. I do use this for my I/O logic reasoner. [Steen]
2. Give only a "yes, finite", indicating that there is a finite model.
3. Output a model in some form
   • In the case of a countermodel for a conjecture, one would like to have some concrete representation of it to see why the theorem cannot be proved. [Claessen]
   • Sometimes it is very easy to find satisfiability (a saturation) with ordered resolution even if there is a finite model. [Tammet]
   • Regardless of the cardinalities, applications that use ATP systems to find models typically need an explicit model with a domain and symbol mapping. [Sutcliffe]
4. Output a finite model in some form
   • Finite models are used to evaluate other clauses. [McCune]
   • It's better to require the output of a finite model as this can be easily checked by other systems. [Zhang]
   • It is not enough to know that there is a solution; one would like to know what the solution is. [Claessen]

Representation of Interpretations

• If the interpretation does not explicitly represent the mapping for a given symbol, then all possible mappings are implied, i.e., it's a set of interpretations. That might not be useful to users.
• Infinite domains are necessary as soon as the formula language contains any numbers on an infinite domain (not arithemetic modulo).
• Infinite domains are also necessary for other (non-numeric) applications, e.g., those that involve modeling time.

• Classical interpretations
  • Interpretations with a finite domain, and the symbol interpretations. These are called finite interpretations. The finite domain can be:
    • Explicitly enumerated.
    • The finite Herbrand Universe of a Herbrand interpretation.
  • Interpretations with an infinite domain, and the symbol interpretations. These are called infinite interpretations. The infinite domain can be:
    • Explicitly generated, e.g., Peano arithmetic terms.
    • Explicitly specified, e.g., the integers.
    • Algebraic numbers (real closed fields)
    • The infinite Herbrand Universe of a Herbrand interpretation.
    • One can explicitly state that it's infinite while leaving open how this is realized, e.g., "in all infinite domains, it holds that ..."
    • Any others?
  • Saturations. Saturations induce Herbrand interpretations.
  • Models that are nearly constant everywhere, as used in the SMT world for model-based quantifier instantiation.
  • Consistent sets of formulae represent families of interpretations. [Steen]
  • You can read off a satisfying assignment from a non-closable tableau, right? [Steen]
  • Any others?
• Non-classical Kripke interpretations
  • Kripke interpretations with a finite number of worlds.
  • Kripke interpretations with an infinite number of worlds. Infinite worlds are necessary when there are, e.g., in alethic modal logic, an infinite number of possibilities; in temporal logics, R is serial (always has a successor) and non-circular etc., so there have to be infinitely many worlds (points in time). [Steen]
  • Within each world of a Kripke interpretation there is a classical interpretation, with the options as above.

Properties of Different Representations

• A finite model with an enumerated domain, and the symbol interpretations.
  • My experience suggests that one would prefer a finite model over a saturation. [Claessen]
  • A finite model can be abbreviated in some way, e.g., if a 30-ary predicate is true for all but three cases, it is enough to mention those 3 cases and a default case. A large predicate table can be expressed in terms of a few smaller ones, e.g., p(X,Y) := q(X) & r(Y). [Claessen]
• A definition of an infinite domain, and the symbol interpretations.
  • The domain must be adequate for interpreting all formulae. [Sutcliffe]
  • I hope it will be OK to specify the interpretation for that subset of an infinite domain that is used, for which the range coincides with the domain. The subset is induced by interpretation of terms, first constants, then inductively by functions. But what if no constants ... add a new constant as done for the Herbrand Universe in a Herbrand interpretation? [Sutcliffe]
  • There are uncountably many interpretations: whatever the language, it will be possible to represent only a small (negligible) subset of all models.
  • The only ATP systems I know of that can produce an explicit infinite domain model are Z3 (Pascal says) and cvc5 (I think!). [Sutcliffe]
• A saturation.
  • A saturation of a set of clauses, created with only logical consequence inferences and simple redundancy, induces the set of Herbrand models of the clauses.
  • A saturation not containing the empty clause induces at least one Herbrand model of the clauses.
  • An empty saturation induces all interpretations, all of which are Herbrand models of the clauses.
  • A saturation induces the same set of Herbrand interpretations as the clauses themselves.
• Opinions about saturations.
  • Hardly a useful artifact. [Sutcliffe]
  • Saturations are pretty much impossible to interpret explicitly in a way that can be used constructively by users. [Sutcliffe]
  • A saturation is not a direct representation of a finite model. [Tammet]
  • A saturation tells you only that models exist, but very little about what they might look like. Take some equational axioms for a group plus a denial of commutativity; the typical saturation gives the complete set of reductions for free groups plus the denial of commutativity, which does help finding an example of a non-commutative group. [McCune]
  • There are classes of problem (including problems where all models are infinite) in which saturation can tell you everything about the models. [McCune]
  • A saturated set of clauses at the end doesn't mean much for other systems. [Zhang]
  • I have never been able to make use of a saturated clause set. [Claessen]
  • The clauses of a saturation could in principle be used for checking whether some later presented finite part of an infinite model is OK. [Tammet]
  • In some sense the saturation does not differ very much from the original clause set: the saturation is also just a clause set, and is typically not a fixpoint for other search strategies. [Tammet]
  • Given a saturation and the system search control, it's sometimes possible to decide if a ground atom is TRUE or FALSE. [Schulz] In the general case you cannot even decide ground atoms. [Tammet]
  • There have been several attempts to improve the representation (Viennese ATP researchers (Leitsch, Baaz, Fermüller etc.), but the improvements are basically still the fixpoint set of clauses. [Tammet]
  • I have never read the proof of completeness of superposition but isn't it the case that a saturation allows to build a model? [Fontaine]
  • An email exchange with Joe Schoisswohl and Cezary Kaliszyk

    A Saturation (S) is a way of writing a Herbrand interpretation
    (HI) of input formulae (I). I learned that a HI consists of:
    
    Domain (D) = The Herbrand Universe (HU), and if the HU is empty add a new
               constant.
    Function map (F) = Identity
    Predicate map (P) = Some way of saying which elements of the Herbrand
               Base (HB) are true/false.
    
    So, simplistically, S can be represented in the TPTP format by providing
    the conjunction of the universally quantified formulae of S. Yeah, I know
    a saturation is modulo the ATP system's ordering, so it might not be
    possible to prove S |= I, but let's gloss over that for now. There might
    be a deeper issue: In the CNF context, S can contain symbols not in I
    (e.g., Skolems), and hence not part of the HU. So formally, S might not
    be an interpretation of I. What problems might arise? I'm thinking of an
    example like ...
    
    Axioms
        ? [X] : p(X)
    HI
        D = {a}
        F = id
        P = p(a) == true
    But ...
        S = {p(sk)}
    
    Here p(sk) |= ? [X] : p(X). Are there any weird cases where things break?
    Can we say that an S that contains symbols not from the I really represents
    a HI of I? Or only a HI of CNF(I), then lean on equisatisfiability to prove
    that "if S |= I then HI |- I" where HI is somehow constructed from S?
    

  • Useful email from Renate Schmidt

    >> During my talk yesterday you indicated that you have or know of ways that
    >> saturations can be useful. Can you point me at what to read, please (or
    >> just tell me the story!). Thanks.
    
    Saturations provide a very useful ways to study modal logics, description
    logics, fragments of FOL, any sets of formulas really. If the saturation is
    ground models can be read off. If they are not ground clauses can be read as
    rules or properties.
    What makes clauses hard to read is nested Skolem terms and clauses that are not
    obviously expressible as first-order formulas.
    
    If structural transformation is done as part of (the translation to FOL for
    non-classical logics and) clausification, and ordered resolution/superposition
    is used, then the saturation will often contain only flat clauses which do not
    contain any nested terms. This can't be generally guaranteed but if the right
    combinations of structural transformation and a refinement of resolution for a
    large number of decidable logics and solvable fragments the saturation will be
    flat (and finitely bounded) and thus readable and useful for gaining insight
    into the problem/the logic and the behaviour of inference.
    Much of the work in developing resolution decision procedures involves
    developing combinations of techniques so that the saturation is well-behaved
    (usually flat).
    
    >>> You may quote me. Please also cite
    >>> https://link.springer.com/chapter/10.1007/978-3-642-37651-1_15
    
    In recent work we developed a saturation method for deciding Boolean conjunctive
    querying and query rewriting for a large class of guarded fragments which
    produces saturations which can be back-translated in FOL, i.e., the saturation
    is readable.
    Reference: https://link.springer.com/article/10.1007/s10817-023-09687-x
    
    We have also investigated how resolution can be used to simulate other inference
    methods, e.g. modal tableau. For this again structural transformation is crucial
    and in the case of tableau we use hyperresolution, where for modal and
    description logics the saturation will be ground and thus nice, because readable
    in the source logic.
    Reference: Section 2 in this paper http://dx.doi.org/10.1016/j.entcs.2010.04.016
    [https://ars.els-cdn.com/content/image/S15710661.gif]
    Simulation and Synthesis of Deduction
    Calculi
    This paper gives an overview of two methods for automatically or
    semi-automatically generating deduction calculi from the semantic specification
    of a …
    dx.doi.org
              

Representation of FOF Finite Interpretations

Representation of FOF Saturation Interpretations

[an error occurred while processing this directive]

Representation of FOF Formulae Interpretations

[an error occurred while processing this directive]

Representation of TFF/TXF Interpretations

[an error occurred while processing this directive]

[an error occurred while processing this directive]

Representation of TXF Interpretations

Representation of THF Interpretations

[an error occurred while processing this directive]

[an error occurred while processing this directive]

Representation of Infinite Interpretations

[an error occurred while processing this directive]

[an error occurred while processing this directive]

[an error occurred while processing this directive]

Representation of Kripke Interpretations

Record world information in interpretation-formulas, using a new defined type $world, a new defined predicate $in_world with type ($world * $o) > $o, a new defined predicate $accessible_world with type ($world * $world) > $o, and a new defined constant $local_world with type $world. Syntactically distinct constants of type $world are known to be unequal. The interpretation in a world is represented as above, with guards used to specify the worlds in which the interpretation is used.

The logic specification of the problem is included as a comment, because the interpretation-formulae under-specify the logic, e.g., it's usually not possible to see whether an interpretation was meant to exemplify a S5 logic specification or a K logic specification - in both cases the concrete model could interpret the accessibility relation as equivalence relation (this is required for S5 but it is also OK for K).

Representation of Finite-Finite Kripke Interpretations - Global Axioms

[an error occurred while processing this directive]

Representation of Finite-Finite Kripke Interpretations - Global and Local Axioms

Representation of Finite-Infinite Kripke Interpretations

Representation of Infinite-Finite Kripke Interpretations

[an error occurred while processing this directive]

[an error occurred while processing this directive]

• The consistency of the interpretation formula cannot be confirmed by any ATP system I have.

Representation of Infinite-Infinite Kripke Interpretations