The PIE system aims at providing an environment for creating complex applications of automated rst-order theorem proving techniques. It is embedded in Prolog. Beyond actual proving tasks, also interpolation and second-order quanti er elimination are supported. A macro feature and a LATEX formula pretty-printer facilitate the construction of elaborate formalizations from small, understandable and documented units. For use with interpolation and elimination, preprocessing operations allow to preserve the semantics of chosen predicates. The system comes with a built-in default prover that can compute interpolants.
1. Tasks beyond Proving. Aside of theorem proving in the literal sense there are various other related tasks which share techniques with rst-order theorem proving and have interesting applications. Basic such tasks are model computation, which became popular in knowledge representation as answer set programming, the computation of rst-order interpolants and second-order quanti er elimination.
From a certain point of view, the opening of rst-order reasoning to second-order extensions seems quite natural: Early technical investigations of rst-order logic have been accompanied by investigations of second-order quanti er elimination for formulas with just unary predicates [Lo15, Sko19, Beh22] (see [Cra08]; for a comprehensive presentation of [Beh22] in this context see [Wer15a]). Today there are many known applications of second-order quanti er elimination and variants of it termed uniform interpolation, forgetting and projection. Aside of the study of modal logics, most of these applications are in knowledge representation and include computation of circumscription, representation of nonmonotonic semantics, abduction with respect to such semantics, forgetting in knowledge bases, and approaches to modularization of knowledge bases based on the notion of conservative extension, e.g., [GO92, LR94, DLS97, Wer04, GLW06, GSS08, GHKS08, LW11, Wer12, Wer13a, KS13, LK14]. Advanced elimination systems are available for description logics, for example the LETHE system [KS15] as well as further implementations of recent techniques for forgetting based on Ackermann's lemma [ZS15, ZS16]. Elimination systems based on rst-order logic have been implemented mainly in the late 1990s [Eng96, Gus96].
Interpolation plays an important role in veri cation [McM05], where it is used mainly on the basis of propositional logic extended with respect to speci c theories. An application area on the basis of full rstorder logic is database query rewriting [Mar07, NSV10, TW11, BBtC13, BtCT14, HTW15]. It seems that so far there have been only specialized techniques applied in this context, in contrast to general rst-order provers. Interpolation for rst-order logic is supported by Princess [BKRW11b, BKRW11a], as well as in some versions/extensions of Vampire [HKV10, HHKV12]. 2. First-Order Logic as Input and Presentation Format. First-order logic can be considered as close enough to natural language to be well suited for humans to express applications. (This is quite di erent from propositional logic, where the formulas input to SAT solvers are typically the output of some encoding mechanism of the application problem. Accordingly, in the DIMACS format commonly used as input for SAT solvers logic atoms are just represented by natural numbers.) Compared to Prolog notation, readability of rst-order formulas can in some cases be improved if functor arguments are not encapsulated by parentheses and not separated by commas, which however requires predeclaration of functor arities. The textbook [EFT84], for example, would write pfxy instead of p(f(x); y). Pretty-printing, where formula structure is re ected in indentation substantially facilitates readability of longer formulas. LATEX provides professional formula layout and seems the format of choice for the presentation of formalizations.
The TPTP syntax allows formulas to be read in by Prolog systems, which is very convenient for Prolog implementations of further formula manipulation. The TPTP tools also include a pretty-printer for that syntax. There are two subtle mismatches of the TPTP syntax and Prolog: TPTP formula variables are represented as Prolog variables, although their scoping is di erent (quanti er arguments vs. clauses); in the ISO Prolog standard unfortunately the character ! is, unlike ?, not of type \graphic", e ecting that universal and existential TPTP quanti er symbols, which are based on ! and ?, can not be handled in exact analogy, and that a != b has to be read in as =(!(a),b). 3. Stepwise Construction of Larger Formalizations. Comprehensibility of even modest-sized formalizations can be improved greatly by using labels, speaking names, for the involved subformulas. In analogy to procedure names, labels are particularly versatile if they can be used with parameters. Such labels also facilitate the re-use of formulas and indicate similarities of related formalizations.
The TPTP requires symbolic names as formula identi ers whose scope is the respective proving problem. They typically appear in proof presentations but are not used to specify the composition of problems from formulas. Shared axiom sets can be expressed in the TPTP by means on an include directive on the le level. 4. Flexibility of Document Granularity. Each proving problem in the TPTP is represented by a le whose name is formed according to a pattern such that application domain and problem format are indicated. While this is very helpful for an archive and testing library, for the development of formalizations it seems more bene cial to follow the traditional approach of the AI programming languages like Lisp and Prolog, which do not tie document granularity { les { with semantic or abstract structural units. However, support for namespaces and symbol rede nition is in such language systems commonly related to les. 5. Integration of Natural Language Text. In many cases it is useful to accompany formalizations with explanatory text. Possibly an interleaved combination of formal and informal material, a form of \literate formalizing", is most adequate for complex formalizations.
TPTP problem les have a structured header that includes an obligatory eld for an English one-line description as well as an optional eld for a longer description. Also a eld for bibliographical references is provided. 6. Sustainability and Repeatability. The usability of documents with complex formalizations should not be limited to a narrow context. Involved mechanized tasks must be repeatable. That a proving problem can be solved not just depends on the choice of the proving system but also on its particular con guration, prone to fail after small changes. This implies that system con gurations known to work have to be precisely recorded. 7. Benchmarks as Side Product. For the computational tasks involved in a complex formalization, it should be possible to generate benchmark documents that can be evaluated independently and in reproducible ways, for example as TPTP problems les. 8. Programming Language Embedding. Embedding in a programming language seems useful: Programming is required to express advanced formula manipulations, including preprocessing or generation of formulas according to repeatedly occurring patterns and to specify ows of control concerning the involved proving and related tasks, as well as postprocessing of their outputs. Prolog, the original basis of the TPTP, seems well suited, in particular since it supports terms as readable and printable data structures that can be immediately used to represent logic formulas. In addition, speci cally the SWI Prolog system comes with very good interfaces to XML and RDF, which are common as exchange formats for large fact bases. 9. Integration of Large Axiom Sets and Fact Bases. Some applications, in particular in common sense reasoning, include large sets of axioms, such as, for example, the excerpts of CYC included in the TPTP, or fact bases such as YAGO, DBPedia and GND, which are available in RDF format. Naming of axioms/facts is irrelevant for these. A human user typically sees only a small fraction of them that is exposed in a proof.
TPTP v6.3.0 includes ve subsets of CYC ranging form 100 up to more than 3 million axioms, where only the second smallest with 8000 axioms was used in the 2015 CASC-25. Seemingly that is the one that can be handled without any special mechanisms by most modern rst-order provers. With LTB the CASC also provides a dedicated division for problems with large shared axiom sets, currently extracted from libraries formalized with interactive proving systems. In the competition, provers are allowed to perform o ine tuning with the shared axioms and example problems.
These issues are addressed by the PIE system with the features and components described in Sect. 2. In the conclusion, Sect. 3, some related work is brie y discussed and an outlook is given. An example that illustrates the use of PIE is provided as Appendix A. Development snapshots of the system with some further examples can be obtained under GNU General Public License from
http://cs.christophwernhard.com/pie/. 2 2.1
The PIE system is the succesor of ToyElim [Wer13b], which is based on propositional logic and has been used in experiments with applications of second-order operator elimination, such as forgetting, abduction and nonmonotonic reasoning semantics. Both systems are implemented in SWI Prolog. To cope with large formulas, on occasion destructive operations like setarg are used but hidden behind an hash table interface.
It is intended to use PIE from the SWI Prolog environment. Thus, the functionality of the system is provided essentially in form of a library of Prolog predicates. The basic formula syntax of PIE di ers from the TPTP syntax (see also Sect. 1, point 2): A formula with quanti ers is represented by a Prolog ground term. For conjunction and disjunction the operators , and ;, as in Prolog, are used. Implication is represented by -> (unfortunately this operator has due to its role as \if-then-else" in Prolog a stronger default precedence than ;). A clausal formula is represented as list of lists of literals, where variables are Prolog variables. Conversions to and from TPTP rst-order and clausal forms as well as Otter/Prover9/Mace4 syntax are provided. For propositional logic and quanti ed Boolean formulas there are conversions to and from DIMACS and QDIMACS, respectively. Call-interfaces for proving tasks to provers accepting the TPTP or the Prover9 format as well as to SAT and QBF solvers are provided. For propositional elimination tasks there is also a special DIMACS -based interface to Coprocessor [Man12], a SAT preprocessor that can be con gured to perform elimination tasks.
The PIE system includes the Prolog-based rst-order prover CM, described further in Sect. 2.4, which is thus immediately available in a lightweight way, without detour through the operation system and without further installation e ort. Proofs returned by CM can be directly processed with Prolog and allow interpolant extraction. The internals of the prover are easy to modify for experimenting. As a second possibility for interpolation tasks, an interface to Princess [BKRW11b] is envisaged. 2.2 A macro facility is provided, where the macros can have parameters and expand to rst- or second-order formulas. In this way, a macro name can serve not just as a formula label but, more generally, can be used within another formula in subformula position, possibly with arguments.
Pattern matching is used to choose the e ective declaration for expansion, allowing structural recursion in macro declarations. An optional Prolog body in a macro declaration permits expansions involving arbitrary computations. Utility predicates intended for use in these bodies are provided for common tasks, for example, determining the predicates in a formula after expansion. With a macro declaration, properties of its lexical environment, in particular con guration settings that a ect the expansion, are recorded.
Macros provide a convenient way to express properties of predicates, e.g., transitivity, abstractly, and also to express more complex application patterns that can not be stated as de nitions within second-order logic unless predicates in argument position would be permitted. Various practically useful computations can be considered as elimination of second-order operators, in particular, literal forgetting (a form of predicate quanti cation that only a ects predicate occurrences with negative or positive polarity), projection (which is like predicate quanti cation, except that the predicates that are not quanti ed { whose semantics is to be retained { are made explicit) and circumscription. The macro mechanism allows to use dedicated operator notation for these on the user level, whereas on the system level predicate quanti cation is the only second-order operator that needs to be supported. 2.3
LATEX Document Generation A formula pretty-printer is available that outputs Prolog-readable syntax as well as LATEX. In addition to formula indentation, the LATEX pretty-printer converts numbers and single characters separated by an underscore at the end of Prolog functor names to subscripts in LATEX. A brief syntax as indicated in Sect. 1, point 2, is optionally available for in- and output of formulas.
Prolog-readable les with macro declarations can be translated to LATEX documents which contain the prettyprinted declarations, all text within specially marked comments, and all outputs produced by calls wrapped in a special Prolog predicate that indicates evaluation at \printtime". Utility predicates for tasks like proving, interpolation and elimination are provided that pretty-print solutions in LATEX at \printtime", and in Prolog when invoked normally. 2.4
The included prover CM was originally written in 1992, based on [Sti88] but as compiler to Prolog instead of Lisp. The underlying calculus can be understood as model elimination, as clausal tableau construction, or as the connection method. The leanCoP prover [Ott10], also implemented in Prolog, is based on the same calculus and regularly takes part in the CASC competitions. Re-implementations of leanCoP have recently found interest to study new techniques [Kal15, KU15]. A conceptual di erence to leanCoP is that CM proceeds in a two-step way, by rst compiling the proving problem. This makes the prover less exible at runtime, but the possibility to inspect the output of the compiler on its own contributes to robustness and facilitates experimenting with modi cations. The prover had been revised in 1997 [DW97] and recently in 2015 where it has been ported to SWI Prolog, combined with some newly implemented preprocessing operations and improved with the problems of the 2015 CASC competition, CASC-25 , taken as yardstick. For the CASC-25 problems in the rst-order no equality (FNE) category it performs better than leanCop and iProver Modulo but worse than CVC4. For the CASC-25 problems in the rst-order with equality (FEQ) category it performs signi cantly worse than leanCop but better than iProver Modulo. More information on the prover and the evaluation details are available at http://cs.christophwernhard.com/pie/cmprover/. 2.5
A number of implemented preprocessing operations is included, most of them currently for clausal inputs. While some of these preserve equivalence, for example conventional CNF transformation (if function introduction through Skolemization is disregarded), others preserve equivalence just with respect to a set of predicates p1; : : : pn, that is, inputs F and outputs G satisfy the second-order equivalence 9q1 : : : 9qm F 9q1 : : : 9qm G;
(1) where q1; : : : ; qm are all involved predicates with exception of p1; : : : pn. Such conversions clearly also preserve equi-satis ability, which corresponds just to the special case where n = 0. Keeping track of the predicates p1; : : : ; pn whose semantics is to preserve is needed for preprocessing in applications like interpolation and secondorder quanti er elimination. (The Riss SAT solver and the related preprocessor Coprocessor [Man12] also support this.) Some preprocessing conversions allow, moreover, to keep track of predicate semantics with respect to just their occurrences with positive or negative polarity, which is useful for Lyndon interpolation (Sect. 2.6) and literal forgetting (Sect. 2.2).
Implemented preprocessing methods that preserve equivalence with respect to a given set of predicates include a variant of the Plaisted-Greenbaum transformation, a structural hashing transformation that identi es two predicates (or one predicate with the negation of another) in the case where both have equivalent non-recursive and easily detectable \semi-de nitions" (the, say, positive \semi-de nition" of the predicate p is obtained by taking all clauses containing a positive literal with predicate p and removing these literals, equivalence (4) below can be used to justify this transformation semantically), and elimination of predicates in cases where this does not lead to a substantial increase of the formula size. 2.6
A Craig interpolant for two given rst-order formulas F and G such that (F ! G) is valid is a rst-order formula H such that (F ! H) and (H ! G) are valid and H contains only symbols (predicates, functions, constants, free variables) that occur in both F and G. Craig's interpolation theorem ensures the existence of such interpolants. The PIE system supports the computation of Craig interpolants from closed clausal tableaux with a variant of the tableau-based interpolant construction method from [Smu95, Fit95]. (It seems that this method has not been reviewed in the recent literature on interpolation for rst-order logic in automated systems, e.g., [HKV10, BKRW11a, BJ15].)
Suitable clausal tableaux are constructed by the CM prover. Interpolant construction can there be done entirely by pre- and postprocessing, without requiring alterations to the core prover. The preprocessing includes simpli cations as outlined in Sect. 2.5. Also the Hyper hypertableau prover [PW07] produces proof terms that can be converted to tableaux, but this is not fully worked out in the current implementation.
The constructed interpolants strengthen the requirements for Craig interpolants in that they are actually Lyndon interpolants, that is, predicates occur in them only in polarities in which they occur in both of the two input formulas. Symmetric interpolation, a generalization of interpolation described in [Cra57, Lemma 2] and called symmetric, e.g., in [McM05, Sect. 5], is supported, implemented by computing a conventional interpolant for each of the input formulas, corresponding to the induction suggested in [Cra57]. Handling of functions (with exception of individual constants) is not supported in the current implementation. It seems possible to implement this by a relational translation of the functions that is reversed on the output. 2.7
In some cases second-order formalizations are convertible to rst-order logic but more concise than their rst-order counterparts. This suggests to use preprocessors that produce rst-order outputs to handle such second-order inputs. The following equivalence is analogous to the familiar e ect of Skolemization of individual variables quanti ed by outermost quanti ers but applies to predicate variables: 9p1 : : : 9pn F [p1; : : : ; pn] j= 8q1 : : : 8qm G[q1 : : : ; qm] i F [p01; : : : ; p0n] j= G[q10 : : : ; qm0]; (2) where F [p01; : : : ; p0n] is obtained from F [p1; : : : ; pn] by replacing all occurrences of predicates pi for 1 i n with fresh predicates p0i and, analogously, G[q10 : : : ; qm0] from G[q1 : : : ; qm] by replacing qi for 1 i m with fresh qi0. The left side of (2) is a second-order entailment, the right side a rst-order entailment. This pattern occurs in the characterization of de nability and computation of de nientia by interpolation (see Appendix A for an example), where advantages of the second-order formulation are that predicate renaming is hidden by quanti cation and that a relation to the strongest necessary and weakest su cient condition [Lin01, DLS01, Wer12], which are essentially second-order concepts, is made explicit.
Moving second-order quanti ers outward can be necessary to achieve a form matching the left side of (2). Aside of the equivalence preserving quanti er movement operations familiar from rst-order quanti ers, the following second-order equivalence, \Ackermann's quanti er switching", due to [Ack35b] can be useful there: 8x9p F [pt1; : : : ; ptm] 9q8x F [qxt1; : : : ; qxtm];
(3) where F [pt1; : : : ; ptm] is a second-order formula in which x only occurs free and p is a predicate of arity n 0 with exactly the m indicated occurrences, instantiated with n-ary argument sequences t1 to tm and F [qxt1; : : : ; qxtm] is like F [pt1; : : : ; ptm] except that the occurrences of p are replaced by occurrences of a fresh predicate q of arity n + 1, applied on the original argument sequences ti prepended by x. Applied in the converse direction than displayed here, the equivalence (3) can help to facilitate second-order quanti er elimination by simplifying the argument formula of the predicate quanti er, leading for example to an elimination-based decision method for the description logic ALC [Wer15b]. The current implementation of PIE includes automatic handling of second-order quanti ers in proving tasks according to (2). More advanced preprocessing is planned. 2.8
Second-order quanti er elimination means to compute for a given formula with second-order quanti ers, that is, quanti ers upon predicate or function symbols, an equivalent rst-order formula. (For functions an arity > 0, in contrast to individual constants, is assumed here.)
For Boolean quanti er elimination, that is, second-order quanti er elimination on the basis of propositional logic, several methods were already available in the ToyElim system: expanding subformulas with the Shannon expansion followed by simpli cations (a more advanced version of this method is described in [Wer09]), and for clausal formulas a resolution-based method as well and a call-interface to Coprocessor [Man12], a SAT preprocessor that can be con gured to perform resolution-based elimination. For rst-order logic, the PIE system currently includes a variant of the DLS algorithm [DLS97], which is based on Ackermann's Lemma, the following equivalence due to [Ack35a]: 9p (8x px ! G[x]) ^ F [pt1; : : : ; ptn]
F [G[t1]; : : : ; G[tn]]; (4) where p does not occur in G[x] and does occur in F in exactly the n indicated occurrences which all have positive polarity, and F [G[t1]; : : : ; G[tn]] is obtained from F [pt1; : : : ; ptn] by replacing all occurrences of p with occurrences of G[x] in which x is instantiated to the respective argument ti of p. (It is assumed that x does not occur bound in G[x].) The lemma obviously also holds in a dual version, where the implication is (8x px G[x]) and the occurences in F all have negative polarity. It can be straightforwardly generalized to predicates p with more than a single argument.
The improvement of the second-order quanti er elimination techniques and their integration with the other supported tasks belong to the major issues for the next development steps. 3
Concerning related work based on rst-order proving, the TPTP had already been mentioned in many speci c contexts. For developing certain kinds of advanced and complex mathematical proofs in a human-assisted way, some rst-order systems, notably Otter and Prover9/Mace4, alone seem suitable by providing control features such as weighting and hints. The most ambitious approach for a working environment around rst-order provers so far seemed to be the ILF project in the 1990s, targeted at human users and mathematical applications. It was centered around an advanced proof conversion with LATEX presentation in textbook style [DGH+94, Dah98]. Further goals were a mathematical library based on Mizar and an embedding into the Mathematica environment [DW97, DHHW98]. The goals of PIE are much more modest. The main focus is not on proofs but on formulas, possibly reduced by elimination and normalized in certain ways. In the conception of the ILF Mathematical Library there was a somewhat ad hoc pragmatic break between syntactic preselection of possibly relevant axioms and their semantic processing by provers. It is the hope that second-order techniques justify a more thoroughly semantic approach to modularization and retrieval from formalized knowledge bases.
It is planned to use PIE embedded into another Prolog-based system that provides knowledge based support for scholarly editing [KW16a, KW16b]. The rst envisaged application there is to control the preprocessing of RDF fact bases through de nienda obtained by interpolation.
As already indicated in Sect. 2.8, the extension of the facilities for second-order quanti er elimination will be a main issue for the next development steps of PIE . Aside of DLS, the second major approach to secondorder quanti er elimination is the resolution-based SCAN algorithm. A variant of this has also been already implemented in PIE but mainly for abstract investigations, without expectation to compete with possible implementations based on dedicated resolution provers. DLS is known to be complete (i.e. terminate successfully) exactly for inputs that satisfy a certain syntactic condition [Con06]. Orthogonal to that condition, there are further cases with known terminating methods, for example, formulas with only unary predicates [Lo15, Beh22] (see also [Wer15b]), \semi-monadic" formulas [Wer15b], and the case where explicitly given ground atoms are \forgotten" [LR94]. Various elimination techniques have thus to be combined for practical application, in a way that ensures completeness for known cases.
A related topic for future research is the exploration of relationships between interpolation and elimination. For example, the objective of one of the preprocessing steps of DLS is to decompose a given formula into a conjunction A ^ B where A contains the predicate p to eliminate just in occurrences with negative polarity and B just with positive polarity, approximately matching the conjunction in the left side of (4). Symmetric interpolation can be used to solve this step in a complete way, that is, whenever there is a decomposition into such A and B, then one is found. Other parallels between interpolation and elimination concern the notion of conservative extension, a relationship between formulas that can be expressed as entailment of an existential second-order formula. For the special case of de nitional extension (see e.g., [Hod97]), also if the extension is not given in the syntactic form of explicit de nitions, the corresponding task can be expressed by rst-order reasoning based on interpolation.
To sum up, the PIE system tries to supplement what is needed to create applications with techniques of automated rst-order proving techniques, not solely in the sense of mathematical theorem proving but considered as general tools of information processing. The main focus are formulas, as constituents of complex formalizations and as results of elimination and interpolation. Special emphasis is made on utilizing some natural relationships between rst- and second-order logics. Key ingredients of the system are macros, LATEX prettyprinting and integration into a programming environment.
This work was supported by DFG grant WE 5641/1-1. [DHHW98] Bernd Ingo Dahn, Andreas Haida, Thomas Honigmann, and Christoph Wernhard. Using Mathematica and automated theorem provers to access a mathematical library. In CADE-15 Workshop on Integration of Deductive Systems, pages 36{43, 1998. [DLS97] Patrick Doherty, Witold Lukaszewicz, and Andrzej Szalas. Computing circumscription revisited: A reduction algorithm. Journal of Automated Reasoning, 18(3):297{338, 1997. [DLS01] Patrick Doherty, Witold Lukaszewicz, and Andrzej Szalas. Computing strongest necessary and weakest su cient conditions of rst-order formulas. In IJCAI-01, pages 145{151. Morgan Kaufmann, 2001. [DW97] Ingo Dahn and Christoph Wernhard. First order proof problems extracted from an article in the Mizar mathematical library. In FTP'97, RISC-Linz Report Series No. 97{50, pages 58{62. Johannes Kepler Universitat, Linz, 1997. [EFT84] Heinz-Dieter Ebbinghaus, Jorg Flum, and Wolfgang Thomas. Mathematical Logic. Springer, 1984. [Eng96] Thorsten Engel. Quanti er elimination in second-order predicate logic. Master's thesis, Max
Planck-Institut fur Informatik, Saarbrucken, 1996. [Fit95] Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer, 2nd edition, 1995. [GHKS08] Bernardo Cuenca Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler. Modular reuse of ontologies: Theory and practice. Journal of Arti cial Intelligence Research, 31(1):273{318, 2008. [GLW06] Silvio Ghilardi, Carsten Lutz, and Frank Wolter. Did I damage my ontology? A case for conservative extensions in description logics. In KR 06, pages 187{197. AAAI Press, 2006. [GO92] Dov Gabbay and Hans Jurgen Ohlbach. Quanti er elimination in second-order predicate logic. In
KR'92, pages 425{435. Morgan Kaufmann, 1992. [GSS08] Dov M. Gabbay, Renate A. Schmidt, and Andrzej Szalas. Second-Order Quanti er Elimination:
Foundations, Computational Aspects and Applications. College Publications, 2008. [Gus96] Joakim Gustafsson. An implementation and optimization of an algorithm for reducing formulae in second-order logic. Technical Report LiTH-MAT-R-96-04, Univ. Linkoping, 1996. [HHKV12] Krystof Hoder, Andreas Holzer, Laura Kovacs, and Andrei Voronkov. Vinter: A Vampire-based tool for interpolation. In APLAS 2012, volume 7705 of LNCS, pages 148{156. Springer, 2012. [HKV10] Krystof Hoder, Laura Kovacs, and Andrei Voronkov. Interpolation and symbol elimination in
Vampire. In IJCAR 2010, volume 6173 of LNCS, pages 188{195. Springer, 2010. [Hod97] Wilfrid Hodges. A Shorter Model Theory. Cambridge University Press, Cambridge, 1997. [HTW15] Alexander Hudek, David Toman, and Grant Wedell. On enumerating query plans using analytic tableau. In TABLEAUX 2015, volume 9323 of LNCS (LNAI), pages 339{354. Springer, 2015. [Kal15] Cezary Kaliszyk. E cient low-level connection tableaux. In TABLEAUX 2015, volume 9323 of
LNCS (LNAI), pages 102{111. Springer, 2015. [KS13] Patrick Koopmann and Renate A. Schmidt. Uniform interpolation of ALC-ontologies using xpoints. In FroCoS 2013, volume 8152 of LNCS (LNAI), pages 87{102. Springer, 2013. [KS15] Patrick Koopmann and Renate Schmidt. LETHE: Saturation-based reasoning for non-standard reasoning tasks. In ORE 2015. CEUR-WS.org, 2015. [KU15] Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly e cient machine learning connection prover.
In LPAR-20, volume 9450 of LNCS, pages 88{96. Springer, 2015. [KW16a] Jana Kittelmann and Christoph Wernhard. Knowledge-based support for scholarly editing and text processing. In DHd 2016 { Konferenzabstracts, pages 176{179. nisaba verlag, 2016. [KW16b] Jana Kittelmann and Christoph Wernhard. Towards knowledge-based assistance for scholarly editing. In AITP 2016 (Book of Abstracts), 2016. [Lin01] Fangzhen Lin. On strongest necessary and weakest su cient conditions. Arti cial Intelligence, 128:143{159, 2001. [LK14] Michel Ludwig and Boris Konev. Practical uniform interpolation and forgetting for ALC TBoxes with applications to logical di erence. In KR'14. AAAI Press, 2014. [LR94] Fangzhen Lin and Raymond Reiter. Forget It! In Working Notes, AAAI Fall Symp. on Relevance, pages 154{159, 1994. [LW11] Carsten Lutz and Frank Wolter. Foundations for uniform interpolation and forgetting in expressive description logics. In IJCAI-11, pages 989{995. AAAI Press, 2011. [Lo15] Leopold Lowenheim. U ber Moglichkeiten im Relativkalkul. Mathematische Annalen, 76:447{470, 1915. [Mar07] [McM05] [NSV10] [Ott10] [PW07] [Sko19] [Smu95] [Sti88] [Sut09] [Sut15] [TW11] [Wer04] [Wer09] [Wer12] [Wer13a] [Wer13b] [Wer15a] [Wer15b] [ZS15] [ZS16]
The following pages illustrate the user view on the PIE system with the rendered LATEX output and the corresponding Prolog-readable input document of a short example. Further examples are included with the system distribution and can be inspected on the system Web page.
A.1
PIE Example Document 1
project(S , F )
project(S , (F ∧ G)) → ¬project(S , (F ∧ ¬G)). 2
We specify a background knowledge base:
∀x (qx → px ) ∧ (px → rx ) ∧ (rx → qx ).
To obtain a definiens of ∃x px in terms {q, r} within kb1 we specify an implication with the definiens macro: Defined as
definiens((∃x px ), kb1 , [q, r]).
We now invoke a utility predicate that computes and prints for a given valid implication an interpolant of its antecedent and consequent: Input: ex1 .
Result of interpolation:
∃x qx .
Before we leave that example, we take a look at the expansion of ex 1: (∃p (∀x (qx → px ) ∧ (px → rx ) ∧ (rx → qx )) ∧
(∃x px )) ¬(∃p (∀x (qx → px ) ∧ (px → rx ) ∧ (rx → qx )) ∧ ¬(∃x px )).
→ And we invoke an external prover (the E prover) to validate it: This formula is valid: ex1 . 3
Obtaining the Strongest Definiens with Elimination The antecedent of the implication in the expansion of definiens specifies the strongest necessary condition of G on S within F . In case definability holds (that is, the implication is valid), this antecedent denotes the strongest definiens. In the example it has a first-order equivalent that can be computed by second-order quantifier elimination. ex2 Defined as Input: ex2 .
Result of elimination: project ([q, r], (kb1 ∧ (∃x px ))).
(∀x ¬rx ∨ qx ) ∧ (∀x ¬qx ∨ rx ) ∧ (∃x rx ).
2 ex1 , 2 ex2 , 2 definiens(G, F , S ), 1 kb1 , 1 project (S , F ), 1 /** \title{\textit{PIE} Example Document} \date{} \maketitle */ :- use_module(folelim(support_scratch)). :- set_info_verbosity(50). :- ppl_set_verbosity(7). /** \section{Projection and Definientia} */ def(project(S,F)) :: ex2(S1, F) ::mac_free_predicates(F, S2), mac_subtract(S2, S, S1). /* mac_free_predicates/2 and mac_subtract/2 are utility functions for use in macro definitions def(definiens(G,F,S)) :: project(S, (F , G)) -> ~project(S, (F, ~(G))). /** \section{Obtaining a Definiens with Interpolation} */ /** We specify a background knowledge base: */ def(kb_1, [syntax=brief]) :: all(x, ((qx->px), (px->rx), (rx->qx))). /** \bigskip /** \bigskip /** \bigskip To obtain a definiens of $\exists x\, \f{p}x$ in terms $\{q, r\}$ within $\mathit{kb_1}$ we specify an implication with the $\mathit{definiens}$ macro: */ def(ex_1, [syntax=brief]) :: definiens(ex(x, px), kb_1, [q,r]).
We now invoke a utility predicate that computes and prints for a given valid implication an interpolant of its antecedent and consequent: */ :- ppl_printtime(ppl_ipol(ex_1)).
Before we leave that example, we take a look at the expansion of $\mathit{ex}_1$: */ /** And we invoke an external prover (the \textit{E} prover) to validate it: /** \section{Obtaining the Strongest Definiens with Elimination} */