Alexander Steen
email: alexander.steen@uni-greifswald.de

Geoff Sutcliffe

Pascal Fontaine
email: pascal.fontaine@uliege.be

Jack Mckeown

Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Historically, Automated Theorem Proving (ATP) has, as the name suggests, focused largely on the task of proving theorems from axioms -the derivation of conclusions that follow inevitably from known facts [START_REF] Robinson | Handbook of Automated Reasoning[END_REF]. The axioms and conjecture to be proved (and hence become a theorem) are written in an appropriately expressive logic, and the proofs are often similarly written in logic [START_REF] Sutcliffe | Using the TPTP Language for Writing Derivations and Finite Interpretations[END_REF]. In this work typed first-order logic in the form of [START_REF] Walther | A Many-Sorted Calculus Based on Resolution and Paramodulation[END_REF][START_REF] Schmidt-Schauss | A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation[END_REF][START_REF] Cohn | A More Expressive Formulation of Many Sorted Logic[END_REF], whose expressive power is sufficient for a wide range of topics [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0[END_REF], is used (This work is also applicable to untyped firstorder logic where terms have the type ι and formulae have the type o, and can also be generalized to higher-order logics.) In the last two decades the converse task of disproving conjectures, i.e., proving that a conjecture is not a theorem of the axioms, has become increasingly important. This process depends on finding an interpretation, i.e., a structure that maps terms to domain elements and formulae to truth values. An interpretation that maps a formula to true is a model of the formula. A conjecture is disproved by finding an interpretation that is a model of the axioms, but maps the conjecture to false. A salient application area that harnesses this form of ATP is verification [START_REF] Silva | A Survey of Automated Techniques for Formal Software Verification[END_REF], where a countermodel is used to pinpoint the reason why a proof obligation fails, and correspondingly points to the location of the fault in the system being verified. Other applications of model finding include checking the consistency of an axiomatization [START_REF] Schulz | Detecting Inconsistencies in Large First-Order Knowledge Bases[END_REF], and finding a solution to a problem that is coded as a model finding problem [START_REF] Winker | Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions[END_REF]. This work describes a (new) format for representing interpretations using a TPTP language -Sections 2 and 3.

In addition to ATP systems that produce interpretations (typically models), e.g., Paradox [START_REF] Claessen | New Techniques that Improve MACE-style Finite Model Finding[END_REF], Vampire [START_REF] Kovacs | First-Order Theorem Proving and Vampire[END_REF], and Nitpick [START_REF] Blanchette | Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder[END_REF], there is a need for tools that support examination and use of interpretations. This paper considers the tasks of verifying models and visualizing interpretations, and describes new tools for these tasks -Sections 4 and 5.

Related Work:

In [START_REF] Sutcliffe | Using the TPTP Language for Writing Derivations and Finite Interpretations[END_REF] a TPTP format for interpretations with finite domains was defined, and has been adopted by some ATP systems, e.g., Paradox and Vampire. The SMT-LIB standard [START_REF] Barrett | The SMT-LIB Standard: Version 2[END_REF] defines a format for model output, and commands to inspect models. SAT solvers generally output models as specified by the SAT competitions [START_REF] Järvisalo | The International SAT Solver Competitions[END_REF], in a simple format similar to the DIMACS input format [START_REF] Babic | Satisfiability Suggested Format[END_REF]. Some individual model finding systems have defined their own formats for models, e.g., the output formats of Nitpick and Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF].

Related work on model verification and interpretation visualization is sparse. In personal communications with members of the Vampire team it was revealed that Vampire can internally verify finite models in TPTP format by using the model formulae to evaluate the given formulae. This approach removes the need for theorem proving as part of the verification process, but is limited to finite models. In personal communications with the developer of Paradox he explained his approach, which is to use a trusted model finder to show that the model formulae and the given formulae are together satisfiable. This shows that the model formulae are consistent with the given formulae, but does not verify the model -as the developer said, it is a "poor-man's model verifier!".

For interpretation visualization, the Mace4 model finder [START_REF] Mccune | Mace4 Reference Manual and Guide[END_REF] outputs textual information about the models it finds, including the interpretation of constants as integers, and tables for the function and predicate symbols' interpretations. The tables are naturally limited to symbols of arity up to two (which is just fine for algebras, where Mace4 is often applied). The only graphical visualization tool that has been found is described in [START_REF] Schlyter | Visualization of a Finite First Order Logic Model[END_REF], which provided (past tense -it is no longer available) a visualization of finite first-order interpretations as produced by Paradox. The visualization had some nice features, e.g., showing functions as constructor functions, and reducing the visual clutter when displaying relations with properties such as symmetry, transitivity, etc. In other ways that work was quite different from the visualization described in this work. This paper is organized as follows: Section 2 introduces the TPTP World which provides the framework and languages used in this research. Section 3 discusses the nature of interpretations, and describes the new representation of interpretations using a TPTP language. Section 4 provides the theory for verifying models, and describes the implementation of that theory in a model verification tool. Section 5 introduces a novel way of visualizing interpretations, and proposes a tool for automating the visualization of interpretations written in the TPTP language. Section 6 concludes and discusses plans for future work.

The TPTP World and Languages

The TPTP World [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0[END_REF] is a well established infrastructure that supports research, development, and deployment of ATP systems. The TPTP World includes the TPTP problem library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0[END_REF], the TSTP solution library [START_REF] Sutcliffe | The TPTP World -Infrastructure for Automated Reasoning[END_REF], standards for writing ATP problems and reporting ATP solutions [START_REF] Sutcliffe | Using the TPTP Language for Writing Derivations and Finite Interpretations[END_REF][START_REF] Sutcliffe | The SZS Ontologies for Automated Reasoning Software[END_REF], tools and services for processing ATP problems and solutions [START_REF] Sutcliffe | The TPTP World -Infrastructure for Automated Reasoning[END_REF], and it supports the CADE ATP System Competition (CASC) [START_REF] Sutcliffe | The CADE ATP System Competition -CASC[END_REF]. Various parts of the TPTP World have been deployed in a range of applications, in both academia and industry. Since the first release of the TPTP problem library in 1993, many researchers have used the TPTP World as an appropriate and convenient basis for ATP system research and development. Over the years the TPTP World has provided a platform upon which ATP users have presented their needs to ATP system developers, who have then adapted their ATP systems to the users' needs. The web page https://www.tptp.org provides access to all components.

The TPTP language [START_REF] Sutcliffe | The Logic Languages of the TPTP World[END_REF] is one of the keys to the success of the TPTP World. The language is used for writing both problems and solutions, which enables convenient communication between systems. Originally the TPTP World supported only first-order clause normal form (CNF) [START_REF] Sutcliffe | The TPTP Problem Library: CNF Release v1.2.1[END_REF]. Over the years full first-order form (FOF) [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0[END_REF], typed first-order form (TFF) [START_REF] Sutcliffe | The TPTP Typed First-order Form with Arithmetic[END_REF][START_REF] Blanchette | TFF1: The TPTP Typed First-order Form with Rank-1 Polymorphism[END_REF], typed extended first-order form (TXF) [START_REF] Sutcliffe | TFX: The TPTP Extended Typed First-order Form[END_REF], typed higher-order form (THF) [START_REF] Sutcliffe | Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure[END_REF][START_REF] Kaliszyk | TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism[END_REF], and non-classical forms (NTF)1 [START_REF] Steen | Automated Reasoning in Non-classical Logics in the TPTP World[END_REF] have been added. A general principle of the TPTP language is "we provide the syntax, you provide the semantics". As such, there is no a priori commitment to any semantics for the languages, although in almost all cases the intended logic and semantics are well known. All the typed forms include constructs for arithmetic. TF0 [START_REF] Sutcliffe | The TPTP Typed First-order Form with Arithmetic[END_REF], the monomorphic subform of TFF, is used in this work (see Section 2.1).

The top level building blocks of the TPTP language are annotated formulae. An annotated formula has the form: language(name, role, formula, source, useful info) The languages supported are cnf (clause normal form), fof (first-order form), tff (typed firstorder form), and thf (typed higher-order form). The role, e.g., axiom, lemma, conjecture, defines the use of the formula in an ATP system. In a formula, terms and atoms follow Prolog conventions -functions and predicates start with a lowercase letter or are 'single quoted', and variables start with an uppercase letter. The language also supports interpreted symbols, which either start with a $, e.g., the truth constants $true and $false, or are composed of nonalphabetic characters, e.g., integer/rational/real numbers such as 27, 43/92, -99.66. The logical connectives in the TPTP language are !, ?, ~, |, &, =>, <=, <=>, and < ~>, for the mathematical connectives ∀, ∃, ¬, ∨, ∧, ⇒, ⇐, ⇔, and ⊕ respectively. Equality and inequality are expressed as the infix operators = and !=. The source and useful info are optional. Annotated formulae (using TF0) can be seen in Figures 12345.

The TF0 Language

TF0 is a typed first-order language. The TF0 types are (i) the predefined types $i for individuals and $o for booleans; (ii) the predefined arithmetic types $int, $rat, and $real; (iii) user-defined types declared to be of the kind $tType. Every symbol is declared with a type signature: (i) individual types for variables; (ii) function types from non-boolean argument types to a non-boolean result type; (iii) predicate types from non-boolean argument types to a boolean result. The equality predicates = and != are ad hoc polymorphic over all types. Arithmetic predicates and functions are ad hoc polymorphic over the arithmetic types. Figures 1 and2 are examples of problems in TF0. Their associated (counter)models are discussed in Section 3.

Interpretations

A Tarskian-style interpretation [START_REF] Tarski | Arithmetical Extensions of Relational Systems[END_REF] of formulae in typed first-order logic consists of a non-empty domain of unequal elements for each type used in the formulae (just one domain for untyped logic), and interpretations of the function and predicate symbols with respect to the domains [START_REF] Hunter | Metalogic: An Introduction to the Metatheory of Standard First Order Logic[END_REF][START_REF] Gallier | Logic for Computer Science -Foundations of Automatic Theorem Proving[END_REF]. I ⊢ Φ means the interpretation I is a model of the formula Φ. An interpretation can normally interpret all expressions that can be written in the language of the formulae, but in some circumstances an interpretation can interpret only (at least) the given formulae; such an interpretation is a partial interpretation.

The domains of an interpretation may be finite or infinite. Interpretations with only finite domains are called finite interpretations, and interpretations with one or more infinite domains are called infinite interpretations. Finite domains are commonly explicitly enumerated, but %------------------------------------------------------- ------------------------------------------------------ ------------------------------------------------------ can also take other forms, e.g., the finite Herbrand Universe of a Herbrand interpretation [START_REF] Herbrand | Recherches sur la Théorie de la Démonstration[END_REF]. Infinite domains can take several forms, including being implicitly specified (e.g., some set of algebraic numbers, such as the integers), explicitly generated (e.g., terms representing Peano numbers), and the infinite Herbrand Universe of a Herbrand interpretation.

= H2 ) ) ). %--------------------------------------------------------
In addition to Tarskian-style interpretations that provide explicit symbol interpretation, a Herbrand interpretation can also be embodied in a saturation [START_REF] Bachmair | Resolution Theorem Proving[END_REF], i.e., a fixed point for a set of clauses at which further application of a complete inference system does not generate any new clauses. This approach is adopted in saturation-based ATP systems such as E [START_REF] Schulz | Faster, Higher, Stronger: E 2.3[END_REF], Prover9 [START_REF] Mccune | Prover9[END_REF], Vampire, and Zipperposition [START_REF] Vukmirović | Making Higher-order Superposition Work[END_REF]. While the domain of a saturation is known to be the Herbrand Universe, there is no explicit symbol interpretation that can be used constructively by users. Saturations are thus a less useful form of interpretation. This work considers only Tarskian-style interpretations.

The notions of interpretations, models, partial interpretations, finite interpretations, Herbrand interpretations, etc., are captured in the SZS ontologies [START_REF] Sutcliffe | The SZS Ontologies for Automated Reasoning Software[END_REF], as updated at https: //www.tptp.org/cgi-bin/SeeTPTP?Category=Documents&File=SZSOntology

Representing Interpretations in TF0

As noted in Section 1, a TPTP format for interpretations with finite domains has previously been defined, and was been adopted by some ATP systems. Recently the need for a format for interpretations with infinite domains, and for a format for Kripke interpretations [START_REF] Kripke | Semantical Considerations on Modal Logic[END_REF] of formulae written in the NTF language [START_REF] Steen | Automated Reasoning in Non-classical Logics in the TPTP World[END_REF], led to the development of a new TPTP format for interpretations. The changes allow for multiple interpretations to be given in a single file, which, in the case of typed logics, share type declarations. The underlying principle is unchanged: interpretations are represented as formulae. This provides the basis for verification of models, as explained in Section 4.

The new format uses an interpretation formula. Examples of interpretation formulae can be seen in Figures 3 and4, illustrating the components described next. An interpretation formula is a conjunction of three components: a conjunction of the domain specifications for the types in the given formulae: for each type a type-promotion function that converts domain elements to terms is used to keep the interpretation formula well-typed; each domain specification is a conjunction of:

the domain type, by a formula that makes the type-promotion function a surjection (unless it is unnecessary because the type is defined and is the same as the type in the given formulae, e.g., both are $int); the domain elements (unless implicit from their defined type): if the domain is finite this is a universally quantified disjunction of equalities whose right-hand sides are the terms; if the domain is infinite an existentially quantified formula that captures an infinite disjunction of equalities is used, e.g., for terms representing Peano numbers as the domain elements: ∀I:peano ((I = zero) ∨ ∃P :peano (I = s(P ))); specification of the distinctness of the domain elements (unless implicit from their defined type); a formula making the type-promotion function an injection, which with the surjectivity makes it a bijection. interpretation of the function symbols, as equalities whose left-hand sides are formed from symbols applied to type-promoted domain elements, and whose right-hand sides are type-promoted domain elements; interpretation of the predicate symbols, as literals formed from symbols applied to typepromoted domain elements; positive literals are true and negative literals are false.

The interpretation formula is preceded by the necessary type declarations: the types in the given formulae (except defined types, e.g., $int); the types of the domains (except defined types); the types of type-promotion functions; the types of the domain elements. This representation is also directly usable for untyped first-order logic, where all terms in the given formulae and the interpretation formula are of the same type -"individuals". This obviates the need for type considerations, in particular type-promotion functions are not needed.

Figure 3 is a TF0 interpretation with finite domains -it is a countermodel for the problem in Figure 1. The comments show which parts of the formula specify what aspects of the interpretation. Figure 4 is a TF0 interpretation with an infinite domain -it is a model for the problem in Figure 2. Note that in Figure 4: the defined type $int is the domain type for the formula type person, so that there is no specification of the domain elements and their distinctness; universal quantification is used for the interpretation of function and predicate symbols for an infinite number of argument tuples; the interpretations of function and predicate symbols is not given for argument tuples with negative integers, i.e., this is an example of a partial interpretation.

Model Verification

ATP systems are complex pieces of software, implementing complex calculi, with the end goal being a sound implementation of a sound inference system whose output correctly corroborates the result obtained. The reality is that the complexity leads to incorrectness, and as such verification of ATP systems' outputs is necessary. For theorem proving this means verifying the proof output [START_REF] Sutcliffe | Semantic Derivation Verification: Techniques and Implementation[END_REF], and for model finding this means verifying the model output. In the context of this work the model verification applies to the type declarations and the interpretation formula that represent the model found by the ATP system, and has (at least) the following aspects:

1. Are the type declarations and interpretation formula syntactically well-formed and semantically well-typed? 2. Is the interpretation formula satisfiable? 3. Does the interpretation formula correctly represent the interpretation found by the ATP system? 4. Is the interpretation represented by the interpretation formula a model for the given formulae?

These questions are answered as follows:

1. This can be confirmed using standard parsing and type checking tools, e.g., [START_REF] Van Gelder | Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation[END_REF][START_REF] Horozal | Formal Logic Definitions for Interchange Languages[END_REF].

2. This can be empirically confirmed using a trusted model finder (in the same way the GDV derivation verifier [START_REF] Sutcliffe | Semantic Derivation Verification: Techniques and Implementation[END_REF] uses the Otter system [START_REF] Mccune | Otter 3.3 Reference Manual[END_REF] as a trusted theorem prover).

Confirming that the interpretation formula is satisfiable is almost certainly much easier than finding the model itself, so the system used to check the satisfiability can be weaker and more trusted than the system that found the model. ------------------------------------------------------ %------------------------------------------------------- 3. This cannot be confirmed, as that representation is internal to the ATP system that found the model.

%-----------------------------------------------------

4.

In this work a "semantic" approach is taken, in which the given formulae Φ are proved from the interpretation formula φ using a trusted theorem prover; φ is supplied as an axiom, and Φ as the conjecture to be proved. This approach relies on the proof of soundness below, which shows that if Φ can be proved from φ (written φ |= Φ), then the interpretation I represented by φ is a model of Φ.

Figure 5 shows the verification problem for the problem in Figure 2 and its model in Fig- ure 4. An implementation is available online as the GMV tool in the SystemOnTSTP [START_REF] Sutcliffe | TPTP, TSTP, CASC, etc[END_REF] web interface https://www.tptp.org/cgi-bin/SystemOnTSTP. The tool input is the concatenation of the interpretation and modeled formula, delimited by % SZS output start and end lines. An example that can be used as the "URL to fetch from" in the web interface is https://raw.githubusercontent.com/GeoffsPapers/ModelVerification/main/FOF_Finite.sp.

GMV.p

The proof of soundness is given here for a finite interpretation in untyped first-order logic, where (as explained in Section 3.1) there is no need for type considerations. The proof for typed first-order logic follows exactly the same pattern, but is technically complicated due to the introduction of types and type promotion functions. The extension to infinite domains is quite simple after that, following Section 3.1. ------------------------------------------------------ ------------------------------------------------------

%-

(I) = P & ! [I1: $int,I2: $int] : ( int2person(I1) = int2person(I2) => I1 = I2 ) ) & bob = int2person(0) & ! [I: $int] : child_of(int2person(I)) = int2person($sum(I,1)) & ! [A: $int,D: $int] : ( is_descendant(int2person(A),int2person(D)) <=> $less(A,D) ) ) ). tff(prove_formulae,conjecture, ( ! [A: person,D: person] : ( is_descendant(A,D) => A != D ) & ! [A: person,C: person,G: person] : ( ( is_descendant(A,C) & is_descendant(C,G) ) => is_descendant(A,G) ) & ! [P: person] : is_descendant(P,child_of(P)) & ! [P: person] : ? [C: person] : C = child_of(P) ) ). %-

Proof

Let Σ be an untyped first-order language:

V Σ -The variable symbols, starting in uppercase. F Σ -The function symbols with arity, in the form f /n. P Σ -The predicate symbols with arity, in the form p/n.

The formulae over Σ, F(Σ), are defined as usual.

Let I be an interpretation for Σ: -

D I -A
V Σφ = V Σ -F Σφ = F Σ ∪ D φ -P Σφ = P Σ φ ∈ F(Σ φ ) = D ∨ φ ∧ D ̸ = φ ∧ F ∧ φ ∧ P ∧ φ
, where:

D ∨ φ = ∀X dφ∈Dφ (X = d φ ) D ̸ = φ = {dφ,eφ}⊆Dφ dφ̸ ≡eφ (d φ ̸ = e φ ) F ∧ φ = f ∈FΣ, f I ∈F I (d I,i →d I )∈f I D φ →I (dφ,i)=d I,i D φ →I (dφ)=d I (f (d φ,i ) = d φ ) P ∧ φ = p∈PΣ, p I ∈P I (d I,i →true)∈p I D φ →I (dφ,i)=d I,i p(d φ,i ) ∧ p∈PΣ, p I ∈P I (d I,i →false)∈p I D φ →I (dφ,i)=d I,i ¬p(d φ,i )
Let I φ be an interpretation for Σ φ : -

D Iφ = D I F Iφ = F I ∪ D φ →I P Iφ = P I Lemma. I φ ⊢ φ Proof. To prove I φ ⊢ φ, prove I φ ⊢ D ∨ φ , I φ ⊢ D ̸ = φ , I φ ⊢ F ∧ φ and I φ ⊢ P ∧ φ : For every d Iφ ∈ D Iφ , or equivalently d I ∈ D I : -There is a d φ ∈ D φ such that D φ →I (d φ ) = d I -(X = d φ ) ∈ D ∨ φ -With X set to d I I φ ⊢ (d I = d φ ) iff d I = F Iφ (d φ ) iff d I = D φ →I (d φ ) which is
I φ ⊢ (f (d φ,i ) = d φ ) iff F Iφ (f (d φ,i )) = F Iφ (d φ ) iff f I (D φ →I (d φ,i )) = D φ →I (d φ ) iff f I (d I,i ) = d I which is true from the use of F I in F ∧ φ Thus every equality in F ∧ φ is true, therefore F ∧ φ is true, i.e., I φ ⊢ F ∧ φ
For every (positive) p(d φ,i ) in P ∧ φ :

- Thus if φ |= Φ then I ⊢ Φ.

I φ ⊢ p(d φ,i ) iff P Iφ (p(F Iφ (d φ,i )

Interpretation Visualization

Proof visualization is well-established, with several tools available, e.g., Evonne [START_REF] Alrabbaa | Evonne: Interactive Proof Visualization for Description Logics (System Description)[END_REF] is an interactive proof visualization software for description logics; ProofTree [START_REF] Tews | Proof tree visualization for proof general[END_REF] is a proof visualization tool focused on interactive theorem proving within Coq; Treehehe [START_REF] Battel | Treehehe: An interactive visualization of proof trees[END_REF] was designed generically to visualize any proof tree but currently it supports only a handful of pre-existing proofs and does not allow users to visualize their own proofs; and the Interactive Derivation Viewer (IDV) [START_REF] Trac | An Interactive Derivation Viewer[END_REF] is a tool for visualization of TPTP format proofs. Interpretation visualization, however, has (to the knowledge of the authors) had minimal attention, as noted in Section 1. Visualization of interpretations is useful in areas such as teaching logic, debugging ATP systems, and understanding of a model.

A visualization for TF0 interpretations has been designed in this work, and an initial implementation is available as the IIV tool in SystemOnTSTP. IIV is built on top of IDV, and has benefited from the mature state of IDV. IDV was originally a Java applet, but has since been ported to HTML/JavaScript using GraphViz [START_REF] Ellson | Graphviz -Open Source Graph Drawing Tools[END_REF] for the layout and rendering. IIV has benefited from the mature state of IDV. The implementation is "initial" because it is fully automated for only finite TF0 and FOF interpretations; for infinite interpretations different components of the interpretation formula currently have to be manually extracted into separate annotated formulae, to mimic a derivation that IDV can render.

Figure 6 is the visualization of the finite countermodel in Figure 3, modified so that john is not created equal to the person who got an A. The top row of inverted triangles are the types in the given formulae, while the bottom row of inverted triangles are the types of the domains. The inverted houses are the function and predicate symbols, and the successive rows of ovals are the successive domain element arguments used to specify the symbols' interpretations. Finally, the row of houses and boxes are the interpretations of the symbols applied to those arguments; houses for domain elements and boxes for truth values. Paths from leaf type nodes to root type nodes show the interpretation of symbols and the domain elements. For example, in Figure 6 the type of grade of is grade, and grade of(d john) is interpreted as d f, which is of type d grade in the interpretation formula.

IIV has interactive features: In Figure 6 the cursor is hovering over the lower d john node on the path from created equal to $true, showing that created equal(d john,d john) is interpreted as $true. The nodes above are increasingly darker red (grey if printed) up to the $o node that is the result type of created equal, and increasingly darker blue down to the $o node that is the type of $true. This highlighting provides easy focus on the interpretation of chosen symbols, e.g., hovering over inverted house nodes shows what symbols applied to what domain elements are interpreted as which domain elements and boolean values, and hovering over oval nodes shows how different domain elements affect the interpretation of symbols. This visualization is available in IIV using https://raw.githubusercontent.com/GeoffsPapers/ModelVerification/ main/TFF_Finite.s as the "URL to fetch from", selecting IIV 0.0 as the "System", and clicking the "Process Solution" button.

Figure 7 is the visualization of the infinite model in Figure 4. Here (universally quantified) variables are used to represent an infinite number of domain elements, and built-in arithmetic predicates are used to compute symbols' mappings. The cursor is hovering over the X:$int node, showing how child of(X) is interpreted as $sum(X,1). This visualization is available in IIV using the IIV format file https://raw.githubusercontent.com/GeoffsPapers/ModelVerification/main/ TFF_Integer.s.IIV as the "URL to fetch from" -this file was manually extracted from the infinite model in Figure 4.

Conclusion

This paper describes the new TPTP format for representing Tarskian-style interpretations for formulae in typed first-order logic, using the TPTP TF0 language. It further describes a technique and an implemented tool for verifying models using this representation, and a tool for visualizing interpretations. The research contributes to the advancement of automated reasoning technology for model finding, which has several applications, including verification.

Currently this work is being extended to Kripke interpretations for formulae in non-classical typed first-order logic [START_REF] Steen | Automated Reasoning in Non-classical Logics in the TPTP World[END_REF], using the TPTP NX0 language [START_REF] Sutcliffe | The Logic Languages of the TPTP World[END_REF]. The tool to translate interpretation formulae to the format required for input to the IIV tool is being extended to infinite interpretations. Further inspiration might also lead to improvements to IIV's visualizations, especially for more complex infinite interpretations.

Figure 1 :

 1 Figure 1: A TF0 problem (with a finite countermodel) https://raw.githubusercontent.com/GeoffsPapers/ModelVerification/main/TFF_Finite.p

-Figure 2 :

 2 Figure 2: A TF0 problem (with an infinite model) https://raw.githubusercontent.com/GeoffsPapers/ModelVerification/main/TFF_Infinite.p

  tff(equality_lost,interpretation, %----The domain for man is d_man ( ( ! [M: man] : ? [DM: d_man] : M = d2man(DM) %----The d_man elements are d_john and d_gotA & ! [DM: d_man] : ( DM = d_john | DM = d_gotA ) & $distinct(d_john,d_gotA) %----The type-promoter is a bijection & ! [DM1: d_man,DM2: d_man] : ( d2man(DM1) = d2man(DM2) => DM1 = DM2 ) %----The domain for grade is d_grade %-

  tff(people,interpretation, %----Domain for type person is the integers ( ! [P: person] : ? [I: $int] : int2person(I) = P %----The type-promoter is a bijection & ! [I1: $int,I2: $int] : ( int2person(I1) = int2person(I2) => I1 = I2 ) %----Mapping people to integers. & bob = int2person(0) & ! [I: $int] : child_of(int2person(I)) = int2person($sum(I,1)) %----Interpretation of descendancy & ! [A: $int,D: $int] : ( is_descendant(int2person(A),int2person(D)) <=> $less(A,D) ) ) ).

  -

Figure 4 :

 4 Figure 4: A TF0 interpretation with an infinite domain https://raw.githubusercontent.com/GeoffsPapers/ModelVerification/main/TFF_Infinite.s

-Figure 5 :

 5 Figure 5: The TF0 verification problem for Figures 2 and 4

  https://raw.githubusercontent.com/GeoffsPapers/ModelVerification/main/TFF_Infinite.s.p

  finite set of unequal domain elements. F I -For each f /n ∈ F Σ , a mapping f I : D n I → D I . P I -For each p/n ∈ P Σ , a mapping p I : D n I → {true, false}. Recalling Section 3.1, an interpretation is represented by an interpretation formula, φ. Let: D φ be a set of fresh terms d φ , one for each d I ∈ D I D φ →I be the corresponding mapping from D φ to D I Σ φ be the untyped first-order language:

  true from the selection of d φ For every d Iφ ∈ D Iφ , with X set to d Iφ , a disjunct in D ∨ φ is true, i.e., I φ ⊢ D ∨ φ For every (d φ ̸ = e φ ) in D ̸ = φ :-I φ ⊢ (d φ ̸ = e φ ) iff F Iφ (d φ ) ̸ = F Iφ (e φ ) iff D φ →I (d φ ) ̸ = D φ→I (e φ ) iff d I ̸ = e I which is true from the definition of D I Thus every inequality in D ̸ = φ I is true, therefore D ̸ = φ is true, i.e., I φ ⊢ D ̸ = φ For every (f (d φ,i ) = d φ ) in F ∧ φ :

  )) iff p I (D φ →I (d φ,i )) iff p I (d I,i ) which is true from the use of P I in P ∧ φ Thus every (positive) p(d φ,i ) in P ∧ φ is true. Analogously, every (negative) ¬p(d φ,i ) in P ∧ φ is false. Therefore P ∧ φ is true, i.e., I φ ⊢ P ∧ φ Theorem. Let Φ ∈ F(Σ), I an interpretation for Σ, and φ the interpretation formula for I. If φ |= Φ then I ⊢ Φ. Proof. If φ |= Φ then I φ ⊢ Φ because every model of φ is a model of Φ, and I φ is a model of φ by the Lemma. I φ ⊢ Φ iff I ⊢ Φ because Φ contains no symbols from D φ , and I φ is the same as I with respect to all other symbols.

Figure 6 :

 6 Figure 6: Visualization of the interpretation in Figure 3

Figure 7 :

 7 Figure 7: Visualization of the interpretation in Figure 4

There are many "non-classical logics", including multi-valued logics[START_REF] Augusto | Many-valued Logics: A Mathematical and Computational Introduction[END_REF], paraconsistent logics[START_REF] Priest | Paraconsistent Logic[END_REF], relevance logics[START_REF] Anderson | Entailment: The Logic of Relevance and Necessity[END_REF], etc. In this work we are interested in those that admit Kripke interpretation[START_REF] Kripke | Semantical Considerations on Modal Logic[END_REF], e.g., modal logics[START_REF] Blackburn | Handbook of Modal Logic[END_REF].

& ! [G: grade] : ? [DG: d_grade] : G = d2grade(DG) %----The d_grade elements are d_a and d_f & ! [DG: d_grade]: ( DG = d_a | DG = d_f ) & $distinct(d_a,d_f) %----The type-promoter is a bijection & ! [DG1: d_grade,DG2: d_grade] : ( d2grade(DG1) = d2grade(DG2) => DG1 = DG2 ) ) %----Interpret terms via the type-promoted domain & ( a = d2grade(d_a) & f = d2grade(d_f) & john = d2man(d_john) & grade_of(d2man(d_john)) = d2grade(d_f) & grade_of(d2man(d_gotA)) = d2grade(d_a) ) %----Interpret atoms as true of false & ( created_equal(d2man(d_john),d2man(d_john)) & created_equal(d2man(d_john),d2man(d_gotA)) & created_equal(d2man(d_gotA),d2man(d_john)) & created_equal(d2man(d_gotA),d2man(d_gotA)) )

) ). %- ------------------------------------------------------


Aurelie Jayol

Marion Saly

Patrice Nordmann

Armelle Menard

Laurent Poirel

Veronique Dubois
email: veronique.dubois@u-bordeaux.fr

Aure´lie Jayol

Armelle Me´nard

Ve´ronique Dubois

Hafnia, an enterobacterial genus naturally

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Hafnia spp. are Gram-negative bacilli belonging to the Enterobacteriaceae family. 1 Hafnia isolates have been mainly recovered in mammalian guts and from food. 1 They are rarely isolated from human specimens, even though they may be occasionally opportunistic human pathogens. They are responsible for nosocomial infections including gastroenteritis, urinary tract infections, meningitis, pneumonia, wound infections, soft tissue infections, endophthalmitis and septicaemia. [START_REF] Stanic | 15) and H. paralvei (n " 10) isolates. Isolates are numbered from 1 to 25 and clones are numbered from A to N. 3[END_REF]3 Hafnia spp. harbour a chromosomal ampC gene, encoding a class C b-lactamase that confers resistance to aminopenicillins and narrow-spectrum cephalosporins. 4 Natural antimicrobial susceptibility patterns of Hafnia alvei strains to 69 antimicrobial agents was reported by Stock et al.,4 but polymyxin susceptibility was not tested. Colistin resistance within Hafnia isolates has been rarely reported. [START_REF] Stanic | 15) and H. paralvei (n " 10) isolates. Isolates are numbered from 1 to 25 and clones are numbered from A to N. 3[END_REF][5][6][7] H. alvei was the unique Hafnia species described until a novel species, namely Hafnia paralvei, was introduced in the taxonomy. 8 A study suggested that H. paralvei could be more resistant to colistin than H.alvei isolates. 5 Taking into account the recent subdivision of the Hafnia genus into H. alvei and H. paralvei, our aim was to analyse the distribution of Hafnia species among 25 clinical isolates of Hafnia, to determine their susceptibility to colistin with the broth microdilution (BMD) reference method, and to compare colistin susceptibility methods for determining colistin resistance in the Hafnia genus.

Materials and methods

Bacterial strains and growth conditions

Twenty-five non-duplicated Hafnia isolates recovered from human samples between 1996 and 2016 were included in this study. Those isolates have been collected from private laboratories (community patients) and at the university hospital of Bordeaux (hospitalized patients) (Table 1). They were kept at -80 • C because they were recovered from deep samples or because they were resistant to extended-spectrum cephalosporins. They were cultured on bromocresol purple (BCP) lactose agar and UriSelect 4 (URI4) chromogenic medium (Bio-Rad, Marnes-la-Coquette, France). The Escherichia coli ATCC 25922 strain, susceptible to colistin, was included in all experiments as a quality control.

Bacterial species identification

Isolates were first identified as H. alvei using the MALDI-TOF mass spectrometer version 2.3 Microflex bench-top (Bruker, Champs-sur-Marne, France). As this spectrometer cannot distinguish between the two Hafnia species, the 16S rRNA gene of each isolate was partially amplified with primers 8F (5 0 -AGAGTTTGATCCTGGCTCAG-3 0 ) and 1489R (5 0 -TACCTTGTTACGACTTCA-3 0 ) and sequenced (Eurofins Genomics, Les Ulis, France). Nucleotide sequences were analysed on the LeBiBi website (https://umr5558-bibiserv.univ-lyon1.fr/lebibi/lebibi.cgi) to identify the bacterial species. 9

Phylogenetic analysis

A phylogenetic tree based on 16S rRNA gene sequences was constructed for the 25 Hafnia isolates and two type strains (H. alvei ATCC 13337 T and H. paralvei ATCC 29927 T ) using the neighbour-joining method. 10 The evolutionary distances were computed using the Kimura two-parameter method 11 and evolutionary analyses were conducted using MEGA6. 12 Colistin susceptibility testing Susceptibility testing of colistin was performed using five different methods. Following EUCAST 2017 breakpoints for Enterobacteriaceae, 13 isolates with an MIC of colistin ≤ 2 mg/L were categorized as susceptible although those with MICs . 2 mg/L were categorized as resistant. For the disc diffusion method, EUCAST 2013 disc breakpoints were used, i.e. susceptible if inhibition zone ≥15 mm and resistant if , 15 mm.

BMD

The BMD method, which is the reference technique, was performed according to the CLSI/EUCAST common guidelines (www.eucast.org). BMD panels were prepared in untreated polystyrene trays (Sarstedt, Nu¨mbrecht, Germany), and dilutions of colistin sulphate (Sigma-Aldrich, St Louis, MO, USA) were made in CAMHB (Bio-Rad). This procedure was performed in triplicate and the MICs were read after 16-20 h of incubation at 37 • C.

Disc diffusion method

The disc diffusion test was performed according to the EUCAST 2013 guidelines. The diameter of the inhibition zone was measured after an incubation of 16-24 h at 37

Etest system

Etest strips (AB bioMe´rieux, La Balme-les-Grottes, France) containing a colistin concentration gradient ranging from 0.016 to 256 mg/L were employed as recommended by the manufacturer's guidelines. MICs were read after an incubation of 16-20 h at 37 • C.

Phoenix automated system

The principle of the BD Phoenix automated system (BD Diagnostic Systems, Le Pont de Claix, France) is based on the BMD technique. The bacterial suspension was prepared as recommended by the manufacturer and poured into the Gram-negative panel NMIC-93 (ref. 448282), which contains wells with colistin concentrations ranging from 0.5 to 4 mg/L. The panel was then incubated for 16 h at 37 • C in the Phoenix automated system.

Rapid Polymyxin NP test

Susceptibility testing of colistin was also assessed using the Rapid Polymyxin NP test, which is based on the detection of the glucose metabolism due to bacterial growth in the presence of colistin. 14 Formation of acid metabolites from this glucose metabolism is evidenced by a colour change (orange to yellow) of a pH indicator (red phenol). The Rapid Polymyxin NP test was performed as described previously with a bacterial inoculum with a turbidity equivalent to that of a 3 McFarland standard, a final colistin concentration of 3.75 mg/L and a visual reading after 2 h of incubation at 37 • C. 14

Molecular typing by PFGE analysis

The genetic relatedness of the isolates was assessed by PFGE analysis with SfiI-digested genomic DNA. 15

Nucleotide sequences accession numbers

The nucleotide sequences of the rRNA 16S genes of the H. alvei and H.paralvei strains were registered in GenBank under accession numbers KY849230 to KY849254.

Results and discussion

Fifteen H. alvei and 10 H. paralvei isolates were identified by using 16S rRNA gene sequencing (Table 1).

H. alvei strain 7 (KY849236)

H. alvei strain 15 (KY849244) 0.005 Figure 1. Phylogenetic tree derived from 16S rRNA sequence comparisons of the Hafnia isolates. Phylogenetic analysis of approximately 1400 nt of the 16S rRNA gene of the 25 Hafnia isolates and two type strains was performed using MEGA software version 6.06 12 and the neighbour-joining method. The optimal tree with the sum of branch length " 0.06351829 is shown. The percentage of replicate trees in which the associated taxa clustered together in the bootstrap test (1000 replicates) is shown next to the branches. The tree is not rooted and is drawn to scale, with branch lengths in the same units as those of the evolutionary distances used to infer the phylogenetic tree. The evolutionary distances were computed using the Kimura two-parameter method and are represented in units of the number of base substitutions per site. All positions containing gaps and missing data were eliminated. There were a total of 1398 positions in the final dataset. The 16S rRNA gene of Morganella morganii was used as an unrelated outgroup sequence. All sequences are labelled by species, strain name and/or collection number and accession number in brackets. T , type strain.

Features of the colonies on URI4 and BCP agar plates showed discrepant results between H. alvei and H. paralvei isolates, respectively (Table 1). The combination of those features seems therefore to be sufficient to distinguish H. alvei and H. paralvei species in routine laboratory testing.

The BMD reference method revealed a high rate of colistin resistance (96%) among the 25 Hafnia isolates recovered over a 20 year period (Table 1). Only a single isolate of H. alvei was susceptible to colistin (MIC 0.125 mg/L). The other isolates had colistin MIC values ranging from 4 to 32 mg/L with no Hafnia speciesdependent variation in resistance level. This high rate of colistin resistance was not related to the spread of a clonal strain as the PFGE analysis identified a diversity of clones (14 clones) in our collection (Figure 2 and Table 1). Surprisingly, several isolates of H. alvei seemed to be clonally related (clone A and clone C, Table 1). Considering that isolates belonging to clone A have been recovered over a 20 year period in various laboratories in the Bordeaux area, it is unlikely that they correspond to a single disseminated strain. We therefore suppose that the genetic diversity of the H. alvei isolates is intrinsically less important than that of the H. paralvei isolates (none of the H. paralvei isolates was clonally related). Those results are in agreement with the 16S rRNA gene sequences analysis, which indicated a greater distance between the H.paralvei isolates compared with those of H.alvei.

As expected, a high rate of false susceptibility results (25%) was observed with Etest strips, compared with the BMD reference method. Moreover, none of the isolates was identified as colistin resistant with the disc diffusion method. Those resistance rates were similar to those reported in previous studies using the same diffusion methods. [START_REF] Stanic | 15) and H. paralvei (n " 10) isolates. Isolates are numbered from 1 to 25 and clones are numbered from A to N. 3[END_REF]5 This further highlights that those methods are not reliable for evaluating the colistin susceptibility (www. eucast.org) and may explain why resistance to colistin within the Hafnia genus has been previously underestimated. On the contrary, the results obtained with the Phoenix automated system and the new Rapid Polymyxin NP test fully correlated with the BMD reference method.

Analysis of the 16S rRNA gene sequences on the LeBiBi web site revealed that H. alvei and H. paralvei species belonged to the same cluster, which is closely related to the cluster of the naturally colistin-resistant Serratia genus (data not shown), thus suggesting

Conclusions

Hafnia spp. may be added to the list of enterobacterial species that are naturally resistant to colistin, along with Proteus spp., Providencia spp., Morganella spp. and Serratia spp.

Table 1 .

 1 Origin, susceptibility results and PFGE profile of the Hafnia isolates

	Colour on	Disc	MIC (mg/L)	Rapid

• C. a Identification of the species by 16S rRNA partial sequencing.

paralvei strain 16 (KY849245) 43 H. paralvei strain 17 (KY849246) H. paralvei strain 22 (KY849251) 48 H. paralvei strain 21 (KY849250) H. paralvei strain 23 (KY849252) 65 H. paralvei strain 25 (KY849254) Morganella morganii type strain CIPA231 T , AT CC 25830T (AJ301681) 54 47 60 66 H. paralvei strain 18 (KY849247) 67 H. paralvei strain 19 (KY849248) H. paralvei strain 20 (KY849249) 97 H. paralvei strain 24 (KY849253) H. paralvei type strain AT CC 29927 T (FM179943) H. alvei strain 13 (KY849242) H. alvei strain 14 (KY849243) H. alvei strain 12 (KY849241) H. alvei strain 11 (KY849240) 64 H. alvei strain 10 (KY849239) H. alvei strain 9 (KY849238) H. alvei strain 8 (KY849237) H. alvei strain 4 (KY849233) 99 H. alvei strain 3 (KY849232) H. alvei strain 6 (KY849235) H. alvei type strain AT CC 13337 T (NR_044729) H. alvei strain 1 (KY849230) 61 H. alvei strain 2 (KY849231) H. alvei strain 5 (KY849234) 64

  The subsequent phylogeny analysis revealed that H. alvei and H. paralvei were clearly separated (two main branches highly stable to bootstrap resampling, with bootstrap values of 99 and 97 for H. alvei and H. paralvei, respectively) (Figure1). It should be noted that H. paralvei isolates are more distant from each other than those of H.alvei.

H.

Acknowledgements

We are grateful for the technical assistance of Catherine Andre´. a natural resistance of Hafnia spp. The DNA relatedness of Hafnia spp. with genera naturally resistant to colistin has already been reported by Sproer et al. 16 (relatedness of Hafnia spp. and Serratia spp.) and Dauga 17 (relatedness of Hafnia spp. with the Proteus-Providencia-Morganella cluster).

This colistin-resistant trait may be related to the structural features of the lipopolysaccharide of Hafnia spp. as already described for Serratia spp. 18 and Proteus spp. 19 The unique strain determined as colistin susceptible with the BMD method might be a mutant not expressing its resistant phenotype. Ongoing investigations will contribute to understand the mechanism of intrinsic resistance in Hafnia genus and to identify to what extent the expression of colistin resistance can be modulated in colistin-susceptible strains.

Funding

This work was supported by internal funding of the University of Bordeaux, France, and the University of Fribourg, Switzerland.

Transparency declarations

None to declare.