IJCAR 2014 LNCS PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. Codatatypes are absent from many programming languages and proof assistants. We make a case for their importance by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. The core of the proof establishes an abstract property of possibly infinite derivation trees, independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of first- order logic. The corresponding Isabelle/HOL formalization demonstrates the recently introduced support for codatatypes and the Haskell code generator.

ABSTRACT. We present a focused intuitionistic sequent calculus for higher- order logic. It has primitive support for equality and mixes λ-term con- version with equality reasoning. Classical reasoning is enabled by ex- tending the system with rules for reductio ad absurdum and the axiom of choice. The resulting system is proved sound with respect to Church’s simple type theory. A theorem prover based on bottom up search in the calculus has been implemented. It has been tested on the TPTP higher-order problem set with good results. The problems for which the theorem prover performs best require higher-order unification more fre- quently than the average higher-order TPTP problem. Being strong at higher-order unification the system may serve as a complement to other theorem provers in the field. The theorem prover produces proofs that can be mechanically verified against the soundness proof.

ABSTRACT. We identify a wide family of analytic sequent calculi for propositional non-classical logics whose derivability problem can be uniformly reduced to SAT. The proposed reduction is based on interpreting these calculi using non-deterministic semantics. Its time complexity is polynomial, and, in fact, linear for a useful subfamily. We further study an extension of such calculi with "Next" operators, and show that this extension preserves analyticity and is subject to a similar reduction to SAT. A particular interesting instance of these results is a HORNSAT-based linear-time decision procedure for Gurevich and Neeman's primal infon logic and several natural extensions of it.

ABSTRACT. For quantified Boolean formulas (QBFs), preprocessing is essential to solve many real-world formulas. Application of a preprocessor, however, prevented the extraction of proofs to independently validate correctness of the solver's result. Especially for universal expansion proof checking was not possible so far. In this paper, we introduce a unified proof system based on three simple and elegant quantified asymmetric tautology QRAT rules. In combination with an extended version of universal reduction, they are sufficient to efficiently express all preprocessing techniques used in state-of-the-art preprocessors including universal expansion. Moreover, these rules give rise to new preprocessing techniques. We equip our preprocessor bloqqer with QRAT proof logging and provide a proof checker for QRAT proofs.

ABSTRACT. Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental testing process. It is believed that these techniques exploit the underlying structure of industrial instances. However, there is not a precise definition of the notion of structure. Recently, there have been some attempts to analyze the structure of these formulas in terms of complex networks, with the long-term aim of explaining the success of these SAT solving techniques, and possibly improving them. We study the fractal dimension of SAT instances with the aim of complementing the model that describes the structure of industrial instances. We show that many industrial families of formulas are self-similar, with a small fractal dimension. We also show how this dimension is affected by the addition of learnt clauses during the execution of SAT solvers.

ABSTRACT. A satisfiability problem is very often expressed in a combination of theories, and a very natural approach consists in solving the problem by combining the satisfiability procedures available for the component theories. This is the purpose of the combination method introduced by Nelson and Oppen. However, in its initial presentation, the Nelson-Oppen combination method requires the theories to be signature-disjoint and stably infinite (to guarantee the existence of an infinite model). The notion of gentle theory has been introduced in the last few years as one solution to go beyond the restriction of stable infiniteness, but in the case of disjoint theories. In this paper, we adapt the notion of gentle theory to the non-disjoint combination of theories sharing only unary predicates (plus constants and the equality). Like in the disjoint case, combining two theories, one of them being gentle, requires some minor assumptions on the other one. We show that major classes of theories, i.e Löwenheim and Bernays-Schönfinkel-Ramsey, satisfy the appropriate notion of gentleness introduced for this particular non-disjoint combination framework.

ABSTRACT. Generating the prime implicates of a formula consists in finding its most general consequences. This has many fields of application in automated reasoning, like planning and diagnosis, and although the subject has been extensively studied (and still is) in propositional logic, very few have approached the problem in more expressive logics because of its intrinsic complexity. This paper presents one such approach for flat ground equational logic. Aiming at efficiency, it intertwines an existing method to generate all prime implicates of a formula with a rewriting technique that uses atomic equations to simplify the problem by removing constants during the search. The soundness, completeness and termination of the algorithm are proven. The algorithm has been implemented and an experimental analysis is provided.

ABSTRACT. Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are ``reasonably complete'' even in the presence of free function symbols ranging into a background theory sort. In this paper we consider the case when all variables occurring below such function symbols are quantified over a finite subset of their domains. We present a (non-naive) decision procedure for background theories extended this way on top of black-box decision procedures for the EA-fragment of the background theory. In its core, it employs a model-guided instantiation strategy for obtaining pure background formulas that are equi-satisfiable with the original formula. Unlike traditional finite model finders, it avoids exhaustive instantiation and, hence, is expected to scale better with the size of the domains. Our main results in this paper are a correctness proof and first experimental results.

ABSTRACT. Consequence finding is used in many applications of deduction. This paper develops and evaluates an optimized SMT-based algorithm for computing equality consequences over arbitrary formulas and theories supported by SMT solvers. It is inspired by an application in the SLAyer analyzer, where our new algorithm is commonly 10-100x faster than simpler folklore algorithms. The new algorithm is based on incrementally refining an initially coarse partition, and is entirely driven by models extracted from a solver to maximize the benefit of model generation capabilities. Our new algorithm requires only O(N) solver calls for N terms, but in the worst case creates O(N^2) fresh subformulas. Simpler algorithms, in contrast, require O(N^2) solver calls. Our algorithm demonstrates low space overhead for SLAyer, yet we also describe an asymptotically superior algorithm that requires O(N) solver calls and only O(N log N) fresh subformulas.

ABSTRACT. AProVE is a system for automated termination and complexity proofs of Java, Haskell, Prolog, and term rewrite systems (TRSs). To analyze programs in high-level programming languages, AProVE automatically converts them to TRSs. Then, a wide range of techniques is employed to prove termination and to infer complexity bounds for the resulting TRSs. Finally, the generated proofs can be exported to certify their correctness using automatic theorem proving techniques. For use in software construction, we present an AProVE plug-in for the popular Eclipse software development environment.

ABSTRACT. In this paper, we build upon our previous work on using constrained clauses in order to finitely represent possibly infinite sets of clauses.

We explore theories and theory extensions that are axiomatized by sets of constrained clauses, and we characterize syntactic criteria for their locality. We have previously shown that constrained axiomatizations are local if they are saturated under a version of resolution. The appearing constraints often capture interesting properties like reachability or extensions thereof.

We extend this result by proving that locality of saturated axiomatizations is maintained if we enrich the base theory by introducing new predicates instead of using constraints for these properties. Often, these new predicates are reachability predicates.

Applications of these results include reasoning about data structures; we indicate how the ideas can be adapted for also handling certain theories with greatest/smallest fixpoints.

ABSTRACT. While automated verification of imperative programs has been studied intensively, proving termination of programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that represents all possible runs of the program. This graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.

ABSTRACT. SAT and QBF solving techniques have applications in various areas. SAT-solving has also been applied in the area of formal verification of temporal properties of transition system models. Because of the limited expressive succinctness, complicated verification problems cannot be naturally represented with SAT-formulas succinctly. This paper investigates QBF-applications in this area, aiming at the verification of branching-time temporal logic properties of transition system models. Branching-time temporal logic properties involve operators that may require whether there exist certain kinds of paths starting at different states of a system model. This requires the use of quantifiers in the encoding of such properties. The focus of this paper is on temporal logic properties specified by the extended computation tree logic that allows some sort of fairness, and the main contribution of this paper is a bounded semantics for the extended computation tree logic. Then a QBF encoding of the temporal logic is developed from the definition of the bounded semantics, and then an implementation of QBF-based verification follows from the QBF encoding. Experimental evaluation of the feasibility and the computational properties of such a QBF-based verification algorithm is reported.

ABSTRACT. Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of the form ∀ x.A (for quantifier-free A) to a method generating lemmas of the form ∀ x_1 ... ∀ x_n.A. Moreover, we extend the original method to predicate logic with equality. The new method was implemented and applied to the TSTP proof database. It is shown that the extension of the method to handle equality and quantifier-blocks leads to a substantial improvement of the old algorithm.

ABSTRACT. The proof of many foundational results in structural proof theory, such as the admissibility of the cut rule and the completeness of the focusing discipline, rely on permutation lemmas. It is often a tedious and error prone task to prove such lemmas as they involve many cases. This paper describes the tool Quati which is an automated tool capable of proving a wide range of inference rule permutations for a wide number of proof systems. Given a proof system specification in the form of a theory in linear logic with subexponentials, Quati outputs in LaTeX the permutation transformations for which it was able to prove correctness and also the possible derivations for which it was not able to do so. As illustrated in this paper, Quati's output is very similar to proof derivation figures one would normally find in a proof theory book.

ABSTRACT. We describe an implementation of a new theorem prover for Intuitionistic Propositional Logic based on a sequent calculus with histories due to Corsi and Tassi. The main novelty of the prover lies in its use of dependency directed backtracking for global caching. We analyse the performance of the prover, and various optimisations, in comparison to current state of the art theorem provers and show that it produces competitive results on many classes of formulae.

ABSTRACT. MleanCoP is an automated theorem prover for first-order modal logic. The proof search is based on a prefixed connection calculus and an additional prefix unification, which captures the Kripke semantics of different modal logics. MleanCoP is implemented in Prolog and the source code of the core proof search procedure consists only of a few lines. It supports the standard modal logics D, T, S4, and S5 with constant, cumulative, and varying domain conditions. The most recent version supports heterogeneous multimodal logics and outputs a compact prefixed connection proof. An experimental evaluation shows the strong performance of MleanCoP.

ABSTRACT. We develop a tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL+ of the full Alternating time temporal logic ATL*. The method extends in an essential way a previous developed tableaux-based decision method for ATL and works in 2EXPTIME, which is the optimal worst case complexity of the satisfiability problem for ATL+. We also discuss how suitable parameterizations and syntactic restrictions on the class of input ATL+ formulae can reduce the complexity of the satisfiability problem.

ABSTRACT. The differential temporal dynamic logic dTL² is a logic to specify temporal properties of hybrid systems. It combines differential dynamic logic with temporal logic to reason about the intermediate states reached by a hybrid system. The logic dTL² supports some branching and linear time temporal properties of CTL*. We provide a semantics and a proof system for the logic dTL², and show its usefulness for nontrivial temporal properties of hybrid systems. We take particular care to handle the case of alternating universal dynamic and existential temporal modalities and its dual, solving an open problem formulated in previous work.

ABSTRACT. We investigate the connections between hypersequent rules with context restrictions and Hilbert axioms extending classical (and intuitionistic) propositional logic. We introduce sufficient syntactic conditions for cut elimination in such hypersequent calculi, translations between rules with context restrictions and axioms (and vice versa), and general decidability and complexity results. Our work subsumes many logic-tailored results, entails finite axiomatisability for a number of normal modal logics given by simple frame properties, and provides a method to construct cut-free hypersequent calculi from a set of axioms. As a case study we obtain a new cut-free hypersequent calculus and complexity bound for the logic of uniform deontic frames.

ABSTRACT. We present a clausal resolution-based method for normal modal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms that characterise such systems. We discuss soundness, completeness, and termination of the method. In particular, completeness can be modularly proved by showing that the conclusions of each newly added inference rule ensures that the corresponding conditions on frames hold. Some examples are given in order to illustrate the use of the method.

ABSTRACT. Binary Decision Diagrams (BDDs) have been used to decide satisfiability and validity in various non-classical logics by directly implementing the finite property method for these logics. We instead present a method for using Binary Decision Diagrams as an underlying data structure for implementing the tableau method itself. We demonstrate our method by implementing the standard tableau calculi for automated reasoning in propositional modal logics K and S4, along with extensions to the multiple and inverse modalities of ALCI. We evaluate our implementation of such a reasoner using several K and S4 benchmark sets, as well as some ALC and ALCI ontologies. We show, with comparison to FaCT++ and InKreSAT, that it can compete with other state of the art methods of reasoning in propositional modal logic. We also discuss how this technique extends to tableaux for other propositional logics.

ABSTRACT. We consider the problem of efficiently computing models for satisfiable constraints, in the presence of complex background theories such as floating-point arithmetic (FPA). Model construction has various applications, for instance the automatic generation of test inputs. It is well-known that naive encoding of constraints into simpler theories (for instance, bit-vectors or propositional logic) can lead to a drastic increase in size, and be unsatisfactory in terms of memory and runtime needed for model construction. We define a framework for systematic application of approximations in order to speed up model construction. Our method is more general than previous techniques in the sense that approximations that are neither under- nor over-approximations (or the combination of both) can be used, and shows promising results in practice.

ABSTRACT. Interval Temporal Logic (ITL) is a powerful formalism to reason about sequences of events that can occur simultaneously and in an overlapping fashion. Despite its importance for various application domains, little tool support for automated ITL reasoning is available, possibly also owed to ITL's undecidability.

We consider the bounded satisfiability which approximates finite satisfiability and is only NP-complete. We provide an encoding into SAT that makes use of the power of modern incremental SAT solvers and present a tool which tests an ITL specification for finite satisfiability.

ABSTRACT. We introduce StarExec, a public web-based service built to facilitate the experimental evaluation of logic solvers, broadly understood as automated tools based on formal reasoning. Examples of such tools include theorem provers, SAT and SMT solvers, constraint solvers, model checkers, and software verifiers. The service, running on a compute cluster with 380 processors and 23 terabytes of disk space, is designed to provide a single piece of storage and computing in- frastructure to logic solving communities and their members. It aims at reducing duplication of effort and resources as well as enabling individual researchers or groups with no access to comparable infrastructure. StarExec allows community organizers to store, manage and make available benchmark libraries; competition organizers to run logic solver competitions; and community members to do com- parative evaluations of logic solvers on public or private benchmark problems.

ABSTRACT. This paper introduces Skeptik: a system for checking, compressing and improving proofs obtained by sat- and smt-solvers.

ABSTRACT. Model generation and minimal model generation are useful for tasks such as model checking and for debugging of logical specifications. This paper presents terminating procedures for the generation of models minimal modulo subset-simulation for the modal logic K and all combinations of extensions with the axioms T, B, D, 4 and 5. Our procedures are minimal model sound and complete. Compared with other minimal model generation procedures, our procedures benefit from smaller search spaces and fewer models are returned. To make the models most effective for users, our minimal model criterion is designed to be semantically meaningful, intuitive and contain minimal amount of information. Depending on the logic, termination is ensured by a variation of equality blocking.

ABSTRACT. We describe the Coalgebraic Ontology Logic solver COOL, a generic reasoner that decides the satisfiability of modal formulas (with nominals) with respect to a set of global assumptions --a TBox in Description Logics parlance. The level of generality is that of coalgebraic logic, a logical framework covering a wide range of modal logics, beyond relational semantics. The core of COOL is an efficient unlabelled tableaux search procedure using global caching. Concrete logics are added by implemening the corresponding (one-step) tableaux rules. The logics covered at the moment are (multi-modal) K and KD (i.e., serial relations), graded modal logic and Pauly's Coalition Logic (the next-step fragment of Alternating-time Temporal Logic), plus every logic that arises from the above as a product (modal fusion) or coproduct of the underlying functors, which are handled automatically in a generic way. We compare the performance of COOL with state-of-the-art reasoners.

ABSTRACT. We provide the first comprehensive proof-complexity analysis of different proof systems for propositional circumscription. In particular, we investigate two sequent-style calculi: MLK defined by Olivetti (J. Autom. Reasoning, 1992) and CIRC introduced by Bonatti and Olivetti (ACM ToCL, 2002), and the tableaux calculus NTAB suggested by Niemelä (TABLEAUX, 1996).

In our analysis we obtain exponential lower bounds for the proof size in NTAB and CIRC and show a polynomial simulation of CIRC by MLK. This yields a chain NTAB < CIRC < MLK of proof systems for circumscription of strictly increasing strength with respect to lengths of proofs.

ABSTRACT. We introduce a robust and tractable temporal logic, we call Visibly Linear Temporal Logic (VLTL), which captures the full class of Visibly Pushdown Languages. The novel logic avoids fix points and provides instead natural temporal operators with simple and intuitive semantics. We prove that the complexities of the satisfiability and pushdown model checking problems are the same as for other well known logics, like CARET and the nested word temporal logic NWTL, which in contrast are strictly more limited in expressive power than VLTL. Moreover, formulas of CARET and NWTL can be easily and inductively translated in linear-time into VLTL.

ABSTRACT. We propose a method for forgetting concept and non-transitive roles symbols of SHQ-ontologies, or for computing uniform interpolants in SHQ. A uniform interpolant of an ontology over a specified set of symbols is a new ontology that only uses the specified symbols, and preserves all logical entailments that can be expressed in SHQ using these symbols. Uniform interpolation has applications in ontology reuse, information hiding and ontology analysis, but so far no method for computing uniform interpolants for expressive description logics with number restrictions has been developed. Our results are not only interesting because they allow to compute uniform interpolants of ontologies that are in a more expressive language. Using number restrictions also allows to preserve more information in uniform interpolants of ontologies in less complex logics, such as ALC or EL. The presented method computes uniform interpolants on the basis of a new resolution calculus for SHQ-ontologies, that allows to derive consequences in a goal-oriented manner. The output of our method is expressed using SHQmu, which is SHQ extended with fixpoint operators, to always enable a finite representation of the uniform interpolant.

ABSTRACT. Nowadays, saturation-based reasoners for the OWL EL profile are able to handle large ontologies such as SNOMED very efficiently. However, saturation-based reasoning procedures become incomplete if the ontology is extended with axioms that use features of more expressive Description Logics, e.g., disjunctions. Tableau-based procedures, on the other hand, are not limited to a specific OWL profile, but even highly optimised reasoners might not be efficient enough to handle large ontologies such as SNOMED. In this paper, we present an approach for tightly coupling tableau- and saturation-based procedures that we implement in the OWL DL reasoner Konclude. Our detailed evaluation shows that this combination significantly improves the reasoning performance on a wide range of ontologies.

ABSTRACT. The OWL 2 EL profile is a fragment of the ontology language OWL 2 for which standard reasoning tasks are feasible in polynomial time. Many OWL ontologies, however, fall outside the EL profile and hence profile-specific reasoners are not applicable. Such ontologies, however, typically contain a small number of axioms outside EL, which may have little or no influence on reasoning outcomes. In this paper, we investigate techniques for rewriting non-EL axioms into EL that preserve the outcomes of classification and instance queries and which are applicable to the DL SHOIQ. Furthermore, for Horn ontologies, we devise a technique inspired by EL-reasoning that can be used to reduce the size of pre-models in (hyper)tableau reasoning. We have implemented and extensively tested our techniques with very encouraging results.

ABSTRACT. We introduce the probabilistic Description Logic BEL. In BEL, axioms are required to hold only in an associated context. The probabilistic component of the logic is given by a Bayesian network (BN) that describes the joint probability distribution of the contexts. We study the main reasoning problems in this logic; in particular, we (i) prove that deciding positive and almost-sure entailments is not harder for BEL than for the BN, and (ii) show how to compute the probability, and the most likely context for a consequence.

ABSTRACT. We report on a project to use Otter to find proofs of the theorems in Tarskian geometry proved in Szmielew's part (Part I) of the book by Schwabhäuser, Szmielew, and Tarski. These theorems start with fundamental properties of betweenness, and end with the development of geometric definitions of addition and multiplication that permit the representation of models of geometry as planes over Euclidean fields, or over real-closed fields in the case of full continuity. They include the four challenge problems left unsolved by Quaife, who two decades ago found some Otter proofs in Tarskian geometry. Our methodology was to present each theorem to Otter as an isolated problem, giving it the (negated) theorem as a goal, and the previous theorems (and the axioms) to use. In practice, we had to coax Otter a bit more.

Quaife's four challenge problems were: every line segment has a midpoint; every segment is the base of some isosceles triangle; the outer Pasch axiom (assuming inner Pasch as an axiom); and the first outer connectivity property of betweenness. These are to be proved without any parallel axiom and without even line-circle continuity. These are difficult theorems, the first proofs of which were the heart of Gupta's Ph.~D. thesis under Tarski. Otter proved them all in 2012. Our success, we argue, is due to improvements in techniques of automated deduction, rather than to increases in computer speed and memory.

The theory of Hilbert (1899) can be translated into Tarski's language, interpreting lines as pairs of distinct points, and angles as ordered triples of non-collinear points. Under this interpretation, the axioms of Hilbert either occur among, or are easily deduced from, theorems in the first 11 (of 16) chapters of Szmielew. At the time of writing this abstract, we have proved all but the two axioms about angles, III.3 and III.4, and we will finish that soon. Narboux and Braun have recently checked these same proofs in Coq.

ABSTRACT. In this paper we present NESCOND, a theorem prover for normal conditional logics. NESCOND implements some recently introduced NESted sequent calculi for propositional CONDitional logics CK and some of its significant extensions with axioms ID, MP and CEM. NESCOND also deals with the flat fragment (i.e., without nested conditionals) of the conditional logic CK+CSO+ID, which corresponds to the cumulative logic C introduced by Kraus, Lehmann and Magidor. NESCOND is inspired to the methodology of leanTAP and it is implemented in Prolog. The paper also shows some experimental results, witnessing that the performances of NESCOND are promising. NESCOND is available at http://www.di.unito.it/~pozzato/nescond/

ABSTRACT. The Suggested Upper Merged Ontology (SUMO) is a large, comprehensive ontology stated in higher-order logic. It has co-evolved with a development environment called the Sigma Knowledge Engineering Environment (SigmaKEE). SUMO has been applied to commercial applications in concept extraction and metadata verification. A large and important subset of SUMO can be expressed in first-order logic with equality. To support the knowledge engineer, SigmaKEE has, over time integrated different reasoning systems, either via special modifications to the reasoner or in an ad-hoc manner that requires full re-processing of the full knowledge base for even trivial queries.

To overcome this problem, to create a simpler system configuration that is easier for users to install and manage, and to integrate a state-of-the-art theorem prover we have now integrated Sigma with the E theorem prover. The E distribution includes a simple server version that loads and indexes the full knowledge base, and supports interactive queries via a simple interface based on text streams. No special modifications to E were necessary for the integration, so SigmaKEE have an easy upgrade path to future versions.