Logic for Programming, Artificial Intelligence, and Reasoning

Frontmatter

The TPTP World – Infrastructure for Automated Reasoning

Abstract

The TPTP World is a well known and established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The data, standards, and services provided by the TPTP World have made it increasingly easy to build, test, and apply ATP technology. This paper reviews the core features of the TPTP World, describes key service components of the TPTP World, presents some successful applications, and gives an overview of the most recent developments.

Geoff Sutcliffe

Speed-Up Techniques for Negation in Grounding

Abstract

Grounding is the task of reducing a first order formula to ground formula that is equivalent on a given universe, and is important in many kinds of problem solving and reasoning systems. One method for grounding is based on an extension of the relational algebra, exploiting the fact that grounding over a given domain is similar to query answering. In this paper, we introduce two methods for speeding up algebraic grounding by reducing the size of tables produced. One method employs rewriting of the formula before grounding, and the other uses a further extension of the algebra that makes negation efficient. We have implemented the methods, and present experimental evidence of their effectiveness.

Amir Aavani, Shahab Tasharrofi, Gulay Unel, Eugenia Ternovska, David Mitchell

Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation

Abstract

Abstract interpretation provides a practical approach to verifying properties of infinite-state systems. We apply the framework of abstract interpretation to derive an abstract semantic function for the modal μ-calculus, which is the basis for abstract model checking. The abstract semantic function is constructed directly from the standard concrete semantics together with a Galois connection between the concrete state-space and an abstract domain. There is no need for mixed or modal transition systems to abstract arbitrary temporal properties, as in previous work in the area of abstract model checking. Using the modal μ-calculus to implement CTL, the abstract semantics gives an over-approximation of the set of states in which an arbitrary CTL formula holds. Then we show that this leads directly to an effective implementation of an abstract model checking algorithm for CTL using abstract domains based on linear constraints. The implementation of the abstract semantic function makes use of an SMT solver. We describe an implemented system for proving properties of linear hybrid automata and give some experimental results.

Gourinath Banda, John P. Gallagher

On the Equality of Probabilistic Terms

Abstract

We consider a mild extension of universal algebra in which terms are built both from deterministic and probabilistic variables, and are interpreted as distributions. We formulate an equational proof system to establish equality between probabilistic terms, show its soundness, and provide heuristics for proving the validity of equations. Moreover, we provide decision procedures for deciding the validity of a system of equations under specific theories that are commonly used in cryptographic proofs, and use concatenation, truncation, and xor. We illustrate the applicability of our formalism in cryptographic proofs, showing how it can be used to prove standard equalities such as optimistic sampling and one-time padding as well as non-trivial equalities for standard schemes such as OAEP.

Gilles Barthe, Marion Daubignard, Bruce Kapron, Yassine Lakhnech, Vincent Laporte

Program Logics for Homogeneous Meta-programming

Abstract

A meta-program is a program that generates or manipulates another program; in homogeneous meta-programming, a program may generate new parts of, or manipulate, itself. Meta-programming has been used extensively since macros were introduced to Lisp, yet we have little idea how formally to reason about meta-programs. This paper provides the first program logics for homogeneous meta-programming – using a variant of MiniML\(_e^{\square}\) by Davies and Pfenning as underlying meta-programming language. We show the applicability of our approach by reasoning about example meta-programs from the literature. We also demonstrate that our logics are relatively complete in the sense of Cook, enable the inductive derivation of characteristic formulae, and exactly capture the observational properties induced by the operational semantics.

Martin Berger, Laurence Tratt

Verifying Pointer and String Analyses with Region Type Systems

Abstract

Pointer analysis statically approximates the heap pointer structure during a program execution in order to track heap objects or to establish alias relations between references, and usually contributes to other analyses or code optimizations. In recent years, a number of algorithms have been presented that provide an efficient, scalable, and yet precise pointer analysis. However, it is unclear how the results of these algorithms compare to each other semantically.

In this paper, we present a general region type system for a Java-like language and give a formal soundness proof. The system is subsequently specialized to obtain a platform for embedding the results of various existing context-sensitive pointer analysis algorithms, thereby equipping the computed relations with a common interpretation and verification. We illustrate our system by outlining an extension to a string value analysis that builds on pointer information.

Lennart Beringer, Robert Grabowski, Martin Hofmann

ABC: Algebraic Bound Computation for Loops

Abstract

We present ABC, a software tool for automatically computing symbolic upper bounds on the number of iterations of nested program loops. The system combines static analysis of programs with symbolic summation techniques to derive loop invariant relations between program variables. Iteration bounds are obtained from the inferred invariants, by replacing variables with bounds on their greatest values. We have successfully applied ABC to a large number of examples. The derived symbolic bounds express non-trivial polynomial relations over loop variables. We also report on results to automatically infer symbolic expressions over harmonic numbers as upper bounds on loop iteration counts.

Régis Blanc, Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács

Hardness of Preorder Checking for Basic Formalisms

Abstract

We investigate the complexity of preorder checking when the specification is a flat finite-state system whereas the implementation is either a non-flat finite-state system or a standard timed automaton. In both cases, we show that simulation checking is Exptime-hard, and for the case of a non-flat implementation, the result holds even if there is no synchronization between the parallel components and their alphabets of actions are pairwise disjoint. Moreover, we show that the considered problems become Pspace-complete when the specification is assumed to be deterministic. Additionally, we establish that comparing a synchronous non-flat system with no hiding and a flat system is Pspace-hard for any relation between trace containment and bisimulation equivalence.

Laura Bozzelli, Axel Legay, Sophie Pinchinat

A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae

Abstract

Jeřábek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek’s result: we give a quasipolynomial-time cut-elimination procedure in propositional-logic deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.

Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, Michel Parigot

Pairwise Cardinality Networks

Abstract

We introduce pairwise cardinality networks, networks of comparators, derived from pairwise sorting networks, which express cardinality constraints. We show that pairwise cardinality networks are superior to the cardinality networks introduced in previous work which are derived from odd-even sorting networks. Our presentation identifies the precise relationship between odd-even and pairwise sorting networks. This relationship also clarifies why pairwise sorting networks have significantly better propagation properties for the application of cardinality constraints.

Michael Codish, Moshe Zazon-Ivry

Logic and Computation in a Lambda Calculus with Intersection and Union Types

Abstract

We present an explicitly typed lambda calculus “à la Church” based on the union and intersection types discipline; this system is the counterpart of the standard type assignment calculus “à la Curry.” Our typed calculus enjoys the Subject Reduction and Church-Rosser properties, and typed terms are strongly normalizing when the universal type is omitted. Moreover both type checking and type reconstruction are decidable. In contrast to other typed calculi, a system with union types will fail to be “coherent” in the sense of Tannen, Coquand, Gunter, and Scedrov: different proofs of the same typing judgment will not necessarily have the same meaning. In response, we introduce a decidable notion of equality on type-assignment derivations inspired by the equational theory of bicartesian-closed categories.

Daniel J. Dougherty, Luigi Liquori

Graded Alternating-Time Temporal Logic

Abstract

Graded modalities enrich the universal and existential quantifiers with the capability to express the concept of at least k or all but k, for a non-negative integer k. Recently, temporal logics such as μ-calculus and Computational Tree Logic, Ctl, augmented with graded modalities have received attention from the scientific community, both from a theoretical side and from an applicative perspective. Both μ-calculus and Ctl naturally apply as specification languages for closed systems: in this paper, we add graded modalities to the Alternating-time Temporal Logic (Atl) introduced by Alur et al., to study how these modalities may affect specification languages for open systems.

We present, and compare with each other, three different semantics. We first consider a natural interpretation which seems suitable to off-line synthesis applications and then we restrict it to the case where players can only employ memoryless strategies. Finally, we strengthen the logic by means of a different interpretation which may find application in the verification of fault-tolerant controllers. For all the interpretations, we efficiently solve the model-checking problem both in the concurrent and turn-based settings, proving its PTIME-completeness. To this aim we also exploit also a characterization of the maximum grading value of a given formula.

Marco Faella, Margherita Napoli, Mimmo Parente

Non-oblivious Strategy Improvement

Abstract

We study strategy improvement algorithms for mean-payoff and parity games. We describe a structural property of these games, and we show that these structures can affect the behaviour of strategy improvement. We show how awareness of these structures can be used to accelerate strategy improvement algorithms. We call our algorithms non-oblivious because they remember properties of the game that they have discovered in previous iterations. We show that non-oblivious strategy improvement algorithms perform well on examples that are known to be hard for oblivious strategy improvement. Hence, we argue that previous strategy improvement algorithms fail because they ignore the structural properties of the game that they are solving.

John Fearnley

A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing

Abstract

We present a sound and complete model of lambda-calculus reductions based on structures inspired by modal logic (closely related to Kripke structures). Accordingly we can construct a logic which is sound and complete for the same models, and we identify lambda-terms with certain simple sentences (predicates) in this logic, by direct compositional translation. Reduction then becomes identified with logical entailment.

Thus, the models suggest a new way to identify logic and computation. Both have elementary and concrete representations in our models; where these representations overlap, they coincide.

In a concluding speculation, we note a certain subclass of the models which seems to play a role analogous to that played by the cumulative hierarchy models in axiomatic set theory and the natural numbers in formal arithmetic — there are many models of the respective theories, but only some, characterised by a fully second order interpretation, are the ‘intended’ ones.

Michael Gabbay, Murdoch J. Gabbay

Label-Free Proof Systems for Intuitionistic Modal Logic IS5

Abstract

In this paper we propose proof systems without labels for the intuitionistic modal logic IS5 that are based on a new multi-contextual sequent structure appropriate to deal with such a logic. We first give a label-free natural deduction system and thus derive natural deduction systems for the classical modal logic S5 and also for an intermediate logic IM5. Then we define a label-free sequent calculus for IS5 and prove its soundness and completeness. The study of this calculus leads to a decision procedure for IS5 and thus to an alternative syntactic proof of its decidability.

Didier Galmiche, Yakoub Salhi

An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory

Abstract

In the celebrated Gödel Prize winning papers, Herlihy, Shavit, Saks and Zaharoglou gave topological characterization of waitfree computation. In this paper, we characterize waitfree communication logically. First, we give an intuitionistic epistemic logic k∨ for asynchronous communication. The semantics for the logic k∨ is an abstraction of Herlihy and Shavit’s topological model. In the same way Kripke model for intuitionistic logic informally describes an agent increasing its knowledge over time, the semantics of k∨ describes multiple agents passing proofs around and developing their knowledge together. On top of the logic k∨, we give an axiom type that characterizes sequential consistency on shared memory. The advantage of intuitionistic logic over classical logic then becomes apparent as the axioms for sequential consistency are meaningless for classical logic because they are classical tautologies. The axioms are similar to the axiom type for prelinearity (ϕ ⊃ ψ) ∨ (ψ ⊃ ϕ). This similarity reflects the analogy between sequential consistency for shared memory scheduling and linearity for Kripke frames: both require total order on schedules or models. Finally, under sequential consistency, we give soundness and completeness between a set of logical formulas called waitfree assertions and a set of models called waitfree schedule models.

Yoichi Hirai

Disunification for Ultimately Periodic Interpretations

Abstract

Disunification is an extension of unification to first-order formulae over syntactic equality atoms. Instead of considering only syntactic equality, I extend a disunification algorithm by Comon and Delor to ultimately periodic interpretations, i.e. minimal many-sorted Herbrand models of predicative Horn clauses and, for some sorts, equations of the form s ^l (x) ≃ s ^k (x). The extended algorithm is terminating and correct for ultimately periodic interpretations over a finite signature and gives rise to a decision procedure for the satisfiability of equational formulae in ultimately periodic interpretations.

As an application, I show how to apply disunification to compute the completion of predicates with respect to an ultimately periodic interpretation. Such completions are a key ingredient to several inductionless induction methods.

Matthias Horbach

Synthesis of Trigger Properties

Abstract

In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. In spite of the rich theory developed for temporal synthesis, little of this theory has been reduced to practice. This is in contrast with model-checking theory, which has led to industrial development and use of formal verification tools. We address this problem here by considering a certain class of PSL properties; this class covers most of the properties used in practice by system designers. We refer to this class as the class of trigger properties.

We show that the synthesis problem for trigger properties is more amenable to implementation than that of general PSL properties. While the problem is still 2EXPTIME-complete, it can be solved using techniques that are significantly simpler than the techniques used in general temporal synthesis. Not only can we avoid the use of Safra’s determinization, but we can also avoid the use of progress ranks. Rather, the techniques used are based on classical subset constructions. This makes our approach amenable also to symbolic implementation, as well as an incremental implementation, in which the specification evolves over time.

Orna Kupferman, Moshe Y. Vardi

Semiring-Induced Propositional Logic: Definition and Basic Algorithms

Abstract

In this paper we introduce an extension of propositional logic that allows clauses to be weighted with values from a generic semiring. The main interest of this extension is that different instantiations of the semiring model different interesting computational problems such as finding a model, counting the number of models, finding the best model with respect to an objective function, finding the best model with respect to several independent objective functions, or finding the set of pareto-optimal models with respect to several objective functions.

Then we show that this framework unifies several solving techniques and, even more importantly, rephrases them from an algorithmic language to a logical language. As a result, several solving techniques can be trivially and elegantly transferred from one computational problem to another. As an example, we extend the basic DPLL algorithm to our framework producing an algorithm that we call SDPLL. Then we enhance the basic SDPLL in order to incorporate the three features that are common in all modern SAT solvers: backjumping, learning and restarts.

As a result, we obtain an extremely simple algorithm that captures, unifies and extends in a well-defined logical language several techniques that are valid for arbitrary semirings.

Javier Larrosa, Albert Oliveras, Enric Rodríguez-Carbonell

Dafny: An Automatic Program Verifier for Functional Correctness

Abstract

Traditionally, the full verification of a program’s functional correctness has been obtained with pen and paper or with interactive proof assistants, whereas only reduced verification tasks, such as extended static checking, have enjoyed the automation offered by satisfiability-modulo-theories (SMT) solvers. More recently, powerful SMT solvers and well-designed program verifiers are starting to break that tradition, thus reducing the effort involved in doing full verification.

This paper gives a tour of the language and verifier Dafny, which has been used to verify the functional correctness of a number of challenging pointer-based programs. The paper describes the features incorporated in Dafny, illustrating their use by small examples and giving a taste of how they are coded for an SMT solver. As a larger case study, the paper shows the full functional specification of the Schorr-Waite algorithm in Dafny.

K. Rustan M. Leino

Relentful Strategic Reasoning in Alternating-Time Temporal Logic

Abstract

Temporal logics are a well investigated formalism for the specification, verification, and synthesis of reactive systems. Within this family, alternating temporal logic, Atl ^*, has been introduced as a useful generalization of classical linear- and branching-time temporal logics by allowing temporal operators to be indexed by coalitions of agents. Classically, temporal logics are memoryless: once a path in the computation tree is quantified at a given node, the computation that has led to that node is forgotten. Recently, mCtl ^* has been defined as a memoryful variant of Ctl ^*, where path quantification is memoryful. In the context of multi-agent planning, memoryful quantification enables agents to “relent” and change their goals and strategies depending on their past history. In this paper, we define mAtl ^*, a memoryful extension of Atl ^*, in which a formula is satisfied at a certain node of a path by taking into account both the future and the past. We study the expressive power of mAtl ^*, its succinctness, as well as related decision problems. We also investigate the relationship between memoryful quantification and past modalities and show their equivalence. We show that both the memoryful and the past extensions come without any computational price; indeed, we prove that both the satisfiability and the model-checking problems are 2ExpTime-Complete, as they are for Atl ^*.

Fabio Mogavero, Aniello Murano, Moshe Y. Vardi

Counting and Enumeration Problems with Bounded Treewidth

Abstract

By Courcelle’s Theorem we know that any property of finite structures definable in monadic second-order logic (MSO) becomes tractable over structures with bounded treewidth. This result was extended to counting problems by Arnborg et al. and to enumeration problems by Flum et al. Despite the undisputed importance of these results for proving fixed-parameter tractability, they do not directly yield implementable algorithms. Recently, Gottlob et al. presented a new approach using monadic datalog to close the gap between theoretical tractability and practical computability for MSO-definable decision problems. In the current work we show how counting and enumeration problems can be tackled by an appropriate extension of the datalog approach.

Reinhard Pichler, Stefan Rümmele, Stefan Woltran

The Nullness Analyser of julia

Abstract

This experimental paper describes the implementation and evaluation of a static nullness analyser for single-threaded Java and Java bytecode programs, built inside the julia tool. Nullness analysis determines, at compile-time, those program points where the null value might be dereferenced, leading to a run-time exception. In order to improve the quality of software, it is important to prove that such situation does not occur. Our analyser is based on a denotational abstract interpretation of Java bytecode through Boolean logical formulas, strengthened with a set of denotational and constraint-based supporting analyses for locally non-null fields and full arrays and collections. The complete integration of all such analyses results in a correct system of very high precision whose time of analysis remains in the order of minutes, as we show with some examples of analysis of large software.

Fausto Spoto

Qex: Symbolic SQL Query Explorer

Abstract

We describe a technique and a tool called Qex for generating input tables and parameter values for a given parameterized SQL query. The evaluation semantics of an SQL query is translated into a specific background theory for a satisfiability modulo theories (SMT) solver as a set of equational axioms. Symbolic evaluation of a goal formula together with the background theory yields a model from which concrete tables and values are extracted. We use the SMT solver Z3 in the concrete implementation of Qex and provide an evaluation of its performance.

Margus Veanes, Nikolai Tillmann, Jonathan de Halleux

Automated Proof Compression by Invention of New Definitions

Abstract

State-of-the-art automated theorem provers (ATPs) are today able to solve relatively complicated mathematical problems. But as ATPs become stronger and more used by mathematicians, the length and human unreadability of the automatically found proofs become a serious problem for the ATP users. One remedy is automated proof compression by invention of new definitions.

We propose a new algorithm for automated compression of arbitrary sets of terms (like mathematical proofs) by invention of new definitions, using a heuristics based on substitution trees. The algorithm has been implemented and tested on a number of automatically found proofs. The results of the tests are included.

Jiří Vyskočil, David Stanovský, Josef Urban

Atomic Cut Introduction by Resolution: Proof Structuring and Compression

Abstract

The careful introduction of cut inferences can be used to structure and possibly compress formal sequent calculus proofs. This paper presents CIRes, an algorithm for the introduction of atomic cuts based on various modifications and improvements of the CERes method, which was originally devised for efficient cut-elimination. It is also demonstrated that CIRes is capable of compressing proofs, and the amount of compression is shown to be exponential in the length of proofs.

Bruno Woltzenlogel Paleo

Satisfiability of Non-linear (Ir)rational Arithmetic

Abstract

We present a novel way for reasoning about (possibly ir)rational quantifier-free non-linear arithmetic by a reduction to SAT/SMT. The approach is incomplete and dedicated to satisfiable instances only but is able to produce models for satisfiable problems quickly. These characteristics suffice for applications such as termination analysis of rewrite systems. Our prototype implementation, called MiniSmt, is made freely available. Extensive experiments show that it outperforms current SMT solvers especially on rational and irrational domains.

Harald Zankl, Aart Middeldorp

Coping with Selfish On-Going Behaviors

Abstract

A rational and selfish environment may have an incentive to cheat the system it interacts with. Cheating the system amounts to reporting a stream of inputs that is different from the one corresponding to the real behavior of the environment. The system may cope with cheating by charging penalties to cheats it detects. In this paper, we formalize this setting by means of weighted automata and their resilience to selfish environments. Automata have proven to be a successful formalism for modeling the on-going interaction between a system and its environment. In particular, weighted finite automata (WFAs), which assign a cost to each input word, are useful in modeling an interaction that has a quantitative outcome. Consider a WFA \(\mathcal{A}\) over the alphabet Σ. At each moment in time, the environment may cheat \(\mathcal{A}\) by reporting a letter different from the one it actually generates. A penalty function η:Σ×Σ→IR ^≥ 0 maps each possible false-report to a penalty, charged whenever the false-report is detected. A detection-probability function p:Σ×Σ→[0,1] gives the probability of detecting each false-report. We say that \(\mathcal{A}\) is (η,p)-resilient to cheating if 〈η,p〉 ensures that the minimal expected cost of an input word is achieved with no cheating. Thus, a rational environment has no incentive to cheat \(\mathcal{A}\).

We study the basic problems arising in the analysis of this setting. In particular, we consider the problem of deciding whether a given WFA \(\mathcal{A}\) is (η,p)-resilient with respect to a given penalty function η and a detection-probability function p; and the problem of achieving resilience with minimum resources, namely, given \(\mathcal{A}\) and η, finding the minimal (with respect to ∑  _σ,σ′ η(σ,σ′)·p(σ,σ′)) detection-probability function p, such that \(\mathcal{A}\) is (η,p)-resilient. While for general WFAs both problems are shown to be PSPACE-hard, we present polynomial-time algorithms for deterministic WFAs.

Orna Kupferman, Tami Tamir

Backmatter