nach oben

2013 | Buch

Kapitel lesen Erstes Kapitel lesen

Programming Logics

Essays in Memory of Harald Ganzinger

herausgegeben von: Andrei Voronkov, Christoph Weidenbach

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This Festschrift volume, published in memory of Harald Ganzinger, contains 17 papers from colleagues all over the world and covers all the fields to which Harald Ganzinger dedicated his work during his academic career. The volume begins with a complete account of Harald Ganzinger's work and then turns its focus to the research of his former colleagues, students, and friends who pay tribute to him through their writing. Their individual papers span a broad range of topics, including programming language semantics, analysis and verification, first-order and higher-order theorem proving, unification theory, non-classical logics, reasoning modulo theories, and applications of automated reasoning in biology.

Inhaltsverzeichnis

Frontmatter

Harald Ganzinger’s Legacy: Contributions to Logics and Programming

Abstract

In 2004 Harald Ganzinger was nominated for the Herbrand Award, which he received only two months before he passed away on June 3, 2004. We describe Ganzinger’s scientific achievements. We hope that this paper will also be useful as a reference guide to Ganzinger’s most significant contributions and publications in many areas of computer science.

Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm

Bio-Logics: Logical Analysis of Bioregulatory Networks

Abstract

We discuss different ways of applying logic to analyze the structure and dynamics of regulatory networks in molecular biology. First, the structure of a bioregulatory network may be described naturally using propositional or multi-valued logic. Second, the resulting non-deterministic dynamics may be analyzed using temporal logic and model checking. Third, information on time delays may be incorporated using a refined modeling approach based on timed automata.

Alexander Bockmayr, Heike Siebert

Canonical Ground Horn Theories

Abstract

An abstract framework of canonical inference based on proof orderings is applied to ground Horn theories with equality. A finite presentation that makes all normal-form proofs available is called saturated. To maximize the chance that a saturated presentation be finite, it should also be contracted, in which case it is deemed canonical. We apply these notions to propositional Horn theories – or equivalently Moore families – presented as implicational systems or associative-commutative rewrite systems, and ground equational Horn theories, presented as decreasing conditional rewrite systems. For implicational systems, we study different notions of optimality and the completion procedures that generate them, and we suggest a new notion of rewrite-optimality, that takes contraction by simplification into account. For conditional rewrite systems, we show that reduced (fully normalized) is stronger than contracted (sans redundancy), and accordingly the perfect system – complete and reduced – is preferred to the canonical one – saturated and contracted. We conclude with a survey of approaches to normal-form proofs, saturated, or canonical, systems, and decision procedures based on them.

Maria Paola Bonacina, Nachum Dershowitz

A Generic Functional Representation of Sorted Trees Supporting Attribution

(Haskell Can Do It)

Abstract

Many important tasks and algorithms in computer science build on sorted trees. Typical examples are the translation of programs represented by syntax trees or the processing of (recursive) data structures following some XML schema. In purely functional programming, sorted trees are usually implemented by terms of recursive data types such that a term represents a tree node and the subterms represent its children. The drawback of this representation is that the context of a tree node is not accessible and has to be managed by different means, e.g., by additional arguments of the functions working on the tree.

In this paper, we present a pattern for the realization of sorted trees that overcomes this drawback. The technique is fully declarative. In contrast to competing patterns for trees such as Zippers, it supports pattern matching on the tree data structure. Functions on tree nodes can be used to express the decoration of trees by attribute values in a flexible way. In particular, links between tree nodes can easily be defined and attributions can be modularized into phases with clear interfaces. Techniques adapted from the “Scrap your boilerplate” approach allow for the high-level specification of contextual constraints. We show how our approach can be realized in Haskell and discuss tool support.

Jean-Marie Gaillourdet, Patrick Michel, Arnd Poetzsch-Heffter, Nicole Rauch

The Blossom of Finite Semantic Trees

Abstract

Automated deduction in first-order logic finds almost all its roots in Herbrand’s work, starting with Herbrand’s interpretations, a clausal calculus, and rules for unification. J.A. Robinson’s key contribution was the formulation of resolution and its completeness proof, in which semantic trees were semi-apparent. Robinson and Wos introduced the specific treatment of equality commonly called paramodulation. The systematic introduction of orderings to cut the search space is due to Lankford. Kowalski studied in more details the case of Horn clauses, while Peterson gave the first proof that paramodulation inside variables was superfluous, assuming a term ordering order-isomorphic to the natural numbers. Knuth studied the case of equality unit clauses, under the name of completion. All these works were done by using standard proof techniques, including semantic trees [Kow69].

Jean Goubault-Larrecq, Jean-Pierre Jouannaud

Functional Logic Programming: From Theory to Curry

Abstract

Functional logic programming languages combine the most important declarative programming paradigms, and attempts to combine these paradigms have a long history. The declarative multi-paradigm language Curry is influenced by recent advances in the foundations and implementation of functional logic languages. The development of Curry is an international initiative intended to provide a common platform for the research, teaching, and application of integrated functional logic languages. This paper surveys the foundations of functional logic programming that are relevant for Curry, the main features of Curry, and extensions and applications of Curry and functional logic programming.

Michael Hanus

From Search to Computation: Redundancy Criteria and Simplification at Work

Abstract

The concept of redundancy and simplification has been an ongoing theme in Harald Ganzinger’s work from his first contributions to equational completion to the various variants of the superposition calculus. When executed by a theorem prover, the inference rules of logic calculi usually generate a tremendously huge search space. The redundancy and simplification concept is indispensable for cutting down this search space to a manageable size. For a number of subclasses of first-order logic appropriate redundancy and simplification concepts even turn the superposition calculus into a decision procedure. Hence, the key to successfully applying first-order theorem proving to a problem domain is to find those simplifications and redundancy criteria that fit this domain and can be effectively implemented.

We present Harald Ganzinger’s work in the light of the simplification and redundancy techniques that have been developed for concrete problem areas. This includes a variant of contextual rewriting to decide a subclass of Euclidean geometry, ordered chaining techniques for Church-Rosser and priority queue proofs, contextual rewriting and history- dependent complexities for the completion of conditional rewrite systems, rewriting with equivalences for theorem proving in set theory, soft typing for the exploration of sort information in the context of equations, and constraint inheritance for automated complexity analysis.

Thomas Hillenbrand, Ruzica Piskac, Uwe Waldmann, Christoph Weidenbach

Elimination Techniques for Program Analysis

Abstract

Key ideas in our recent work on automatically generating polynomial equalities and inequalities as invariants/inductive assertions for imperative programs are reviewed. Two approaches based on elimination techniques are briefly discussed. The first approach is algebraic and is based on giving the semantics of programming language constructs in terms of polynomial ideals. The second approach is based on assuming a priori the shapes of inductive assertions of interest and then using quantifier elimination techniques to generate constraints on parameters specifying the shape. The key ideas of these approaches are illustrated through examples.

Deepak Kapur

Narrowing Based Inductive Proof Search

Abstract

We present in this paper a narrowing-based proof search method for inductive theorems. It has the specificity to be grounded on deduction modulo and to yield a direct translation from a successful proof search derivation to a proof in the sequent calculus. The method is shown to be sound and refutationally correct in a proof theoretical way.

Claude Kirchner, Hélène Kirchner, Fabrice Nahon

Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning

Abstract

Inst-Gen is an instantiation-based reasoning method for first-order logic introduced in [18]. One of the distinctive features of Inst-Gen is a modular combination of first-order reasoning with efficient ground reasoning. Thus, Inst-Gen provides a framework for utilising efficient off-the-shelf propositional SAT and SMT solvers as part of general first-order reasoning. In this paper we present a unified view on the developments of the Inst-Gen method: (i) completeness proofs; (ii) abstract and concrete criteria for redundancy elimination, including dismatching constraints and global subsumption; (iii) implementation details and evaluation.

Konstantin Korovin

Common Knowledge Logic in a Higher Order Proof Assistant

Abstract

This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant Coq. The main feature of common knowledge logic is the eponymous modality that says that a group of agents shares a knowledge about a certain proposition in a inductive way. This modality is specified by using a fixpoint approach. Furthermore, from these experiments, we discuss and compare the structure of theorems that can be proved in specific theories that use common knowledge logic. Those structures manifest the interplay between the theory (as implemented in the proof assistant Coq) and the metatheory.

Pierre Lescanne

Constructing Bachmair-Ganzinger Models

Abstract

We give some algorithms for constructing models from sets of clauses saturated by Ordered Resolution (with Selection rules). In the ground case, we give an efficient algorithm for constructing a minimal model. Then we generalize minimal models to preferred models, which may be useful for verification. For the ground case, we also show how to construct all models for a set of clauses saturated by Ordered Resolution, in time polynomial in the number of models. We also generalize our results to nonground models, where we add a restricted splitting rule to our inference rules, and show that for any set of clauses saturated by Ordered Resolution (with Selection), a query about the truth of a particular atom in the model can be decided.

Christopher Lynch

Planning with Effectively Propositional Logic

Abstract

We present a fragment of predicate logic which allows the use of equality and quantification but whose models are limited to finite Herbrand interpretations. Formulae in this logic can be thought as syntactic sugar on top of the Bernays-Schönfinkel fragment and can, therefore, still be effectively grounded into a propositional representation. We motivate the study of this logic by showing that practical problems from the area of planning can be naturally and succinctly represented using the added syntactic features. Moreover, from a theoretical point of view, we show that this logic allows, when compared to the propositional approach, not only more compact encodings but also exponentially shorter refutation proofs.

Juan Antonio Navarro-Pérez, Andrei Voronkov

The Relative Power of Semantics and Unification

Abstract

The OSHL theorem proving method is an attempt to extend propositional theorem proving techniques to first-order logic by working entirely at the ground level. A disadvantage of this approach is that OSHL does not perform unifications between non-ground literals, as resolution does. However, OSHL has the capability to use natural semantics to guide the proof search. The question arises whether the advantage of proof guidance using semantics can make up for the loss of unification between non-ground literals that other methods employ. This question is studied and some evidence is given that a properly chosen semantics causes OSHL to implicitly perform unifications between non-ground levels, suggesting that OSHL may have some of the advantages of theorem proving methods based on unification as well as some of the efficiencies of propositional theorem provers. Some implementation results of OSHL with and without nontrivial semantics are also presented to illustrate its properties.

David A. Plaisted, Swaha Miller

First-Order Resolution Methods for Modal Logics

Abstract

In this paper we give an overview of results for modal logic which can be shown using techniques and methods from first-order logic and resolution. Because of the breadth of the area and the many applications we focus on the use of first-order resolution methods for modal logics. In addition to traditional propositional modal logics we consider more expressive PDL-like dynamic modal logics closely related to description logics. Without going into too much detail, we survey different ways of translating modal logics into first-order logic, we explore different ways of using first-order resolution theorem provers to solve a range of reasoning problems for modal logics, and we discuss a variety of results which have been obtained in the setting of first-order resolution.

Renate A. Schmidt, Ullrich Hustadt

On Combinations of Local Theory Extensions

Abstract

In this paper we study theory extensions in which efficient reasoning is possible. We study local extensions (in which hierarchical reasoning is possible) and give several examples from computer science or mathematics in which such extensions occur in a natural way. We then identify situations in which combinations of local extensions of a theory are again local extensions of that theory. We thus obtain criteria both for recognizing wider classes of local theory extensions, and for modular reasoning in combinations of theories over non-disjoint signatures.

Viorica Sofronie-Stokkermans

Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs

Abstract

We present a framework for local interprocedural shape analysis that computes procedure summaries as transformers of procedure-local heaps (the parts of the heap that the procedure may reach). A main challenge in procedure-local shape analysis is the handling of cutpoints, objects that separate the input heap of an invoked procedure from the rest of the heap, which—from the viewpoint of that invocation—is non-accessible and immutable.

In this paper, we limit our attention to effectively cutpoint-free programs—programs in which the only objects that separate the callee’s heap from the rest of the heap, when considering live reference fields, are the ones pointed to by the actual parameters of the invocation. This limitation (and certain variations of it, which we also describe) simplifies the local-reasoning about procedure calls because the analysis needs not track cutpoints. Furthermore, our analysis (conservatively) verifies that a program is effectively cutpoint-free,

J. Kreiker, T. Reps, N. Rinetzky, M. Sagiv, Reinhard Wilhelm, E. Yahav

Backmatter

Titel: Programming Logics
herausgegeben von: Andrei Voronkov
Christoph Weidenbach
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-37651-1
Print ISBN: 978-3-642-37650-4
DOI: https://doi.org/10.1007/978-3-642-37651-1