eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2007-11-29
7401
1
20
10.4230/DagSemProc.07401.1
article
07401 Abstracts Collection – Deduction and Decision Procedures
Baader, Franz
Cook, Byron
Giesl, Jürgen
Nieuwenhuis, Robert
From 01.10. to 05.10.2007, the Dagstuhl Seminar 07401 ``Deduction and Decision Procedures'' was held in the International Conference and Research Center (IBFI),
Schloss Dagstuhl.
During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar
as well as abstracts of seminar results and ideas
are put together in this paper.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol07401/DagSemProc.07401.1/DagSemProc.07401.1.pdf
Decision Procedures
Deduction
Boolean Satisfiability
First-Order Logic
Integer Arithmetic
Combination of Theories
Satisfiability Modulo Theories Rewrite Systems
Formal Verification
Model Finding
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2007-11-29
7401
1
3
10.4230/DagSemProc.07401.2
article
07401 Executive Summary – Deduction and Decision Procedures
Baader, Franz
Cook, Byron
Giesl, Jürgen
Nieuwenhuis, Robert
Formal logic provides a mathematical foundation for many areas of
computer science. Significant progress has been made in the
challenge of making computers perform non-trivial logical reasoning.
be it fully automatic, or in interaction with humans.
In the last years it has become more and more evident that
theory-specific reasoners, and in particular decision procedures, are
extremely important in many applications of such deduction tools.
General-purpose reasoning methods such as resolution or paramodulation
alone are not efficient enough to handle the needs of real-world
applications.
%
For this reason, the focus of this seminar was on decision procedures,
their integration into general-purpose theorem provers,
and the application of the integrated tools in computer science.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol07401/DagSemProc.07401.2/DagSemProc.07401.2.pdf
Formal Logic
Deduction
Artificial Intelligence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2007-11-29
7401
1
17
10.4230/DagSemProc.07401.3
article
Decision Procedures for Loop Detection
Thiemann, René
Giesl, Jürgen
Schneider-Kamp, Peter
The dependency pair technique is a powerful modular method for automated termination proofs of term rewrite systems. We first show that dependency pairs are also suitable for disproving termination: loops can be detected more easily.
In a second step we analyze how to disprove innermost termination. Here, we present a novel procedure to decide whether a given loop is an innermost loop.
All results have been implemented in the termination prover AProVE.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol07401/DagSemProc.07401.3/DagSemProc.07401.3.pdf
Non-Termination
Decision Procedures
Term Rewriting
Dependency Pairs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2007-11-29
7401
1
2
10.4230/DagSemProc.07401.4
article
From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems
Ghilardi, Silvio
Ranise, Silvio
Nicolini, Enrica
Zucchelli, Daniele
In the first part of our contribution, we review recent results on combined constraint satisfiability for first order theories in the non-disjoint signatures case: this is done mainly in view of the applications to temporal satisfiability and model-checking covered by the second part of our talk, but we also illustrate in more detail some case-study where non-disjoint combination arises. The first case deals with extensions of the theory of arrays where indexes are endowed with a Presburger arithmetic structure
and a length expressing `dimension' is added; the second case deals with the algebraic counterparts of fusion in modal logics. We then recall the basic features of the Nelson-Oppen method and investigate sufficient conditions for it to be complete and terminating in the non-disjoint signatures case: for completeness we rely on a model-theoretic $T_0$-compatibility condition (generalizing stable infiniteness) and for termination we impose a noetherianity requirement on positive constraints chains. We finally supply examples of theories matching these combinability hypotheses.
In the second part of our contribution, we develop a framework for integrating first-order logic (FOL) and discrete Linear time Temporal Logic (LTL). Manna and Pnueli have extensively shown how a mixture of FOL and LTL is sufficient to precisely state verification problems for the class of
reactive systems: theories in FOL model the (possibly infinite) data structures used by a reactive system while LTL specifies its (dynamic) behavior. Our framework for the integration is the following: we fix a theory $T$ in a first-order signature $Sigma$ and consider as a temporal model a sequence $cM_1, cM_2, dots$ of standard (first-order) models of $T$ and assume such models to share the same carrier (or, equivalently, the domain of the temporal model to be `constant'). Following Plaisted, we consider symbols from a subsignature $Sigma_r$ of $Sigma$ to be emph{rigid}, i.e. in a temporal model $cM_1, cM_2, dots$, the
$Sigma_r$-restrictions of the $cM_i$'s must coincide. The symbols
in $Sigmasetminus Sigma_r$ are called `flexible' and their
interpretation is allowed to change over time (free variables are
similarly divided into `rigid' and `flexible'). For model-checking,
the emph{initial states} and the emph{transition relation} are
represented by first-order formulae, whose role is that of
(non-deterministically) restricting the temporal evolution of the
model.
In the quantifier-free case, we obtain sufficient conditions for %undecidability and decidability for both satisfiability and model-checking of safety properties emph{by lifting combination methods} for emph{non-disjoint} theories in FOL: noetherianity and $T_0$-compatibility
(where $T_0$ is the theory axiomatizing the rigid subtheory) gives decidability of satisfiability, whereas $T_0$-compatibility and local finiteness give safety model-checking decidability. The proofs of these decidability results suggest how decision procedures for the constraint satisfiability problem of theories in FOL and algorithms for checking the satisfiability of propositional LTL formulae can be integrated. This paves the way to employ efficient Satisfiability Modulo Theories solvers in the
model-checking of infinite state systems. We illustrate our
techniques on some examples and discuss further work in the area.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol07401/DagSemProc.07401.4/DagSemProc.07401.4.pdf
Non disjoint combination
linear temporal logic
model checking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2007-11-29
7401
1
10
10.4230/DagSemProc.07401.5
article
Implementing RPO and POLO using SAT
Schneider-Kamp, Peter
Fuhs, Carsten
Thiemann, René
Giesl, Jürgen
Annov, Elena
Codish, Michael
Middeldorp, Aart
Zankl, Harald
Well-founded orderings are the most basic, but also most important
ingredient to virtually all termination analyses. The recursive
path order with status (RPO) and polynomial interpretations (POLO)
are the two classes that are the most popular in the termination
analysis of term rewrite systems. Numerous fully automated search
algorithms for these classes have therefore been devised and
implemented in termination tools.
Unfortunately, the performance of these algorithms on all but the
smallest termination problems has been lacking. E.g., recently
developed transformations from programming languages like Haskell
or Prolog allow to apply termination tools for term rewrite systems
to real programming languages. The results of the transformations
are often of non-trivial size, though, and cannot be handled
efficiently by the existing algorithms.
The need for more efficient search algorithms has triggered research
in reducing these search problems into decision problems for
which more efficient algorithms already exist. Here, we introduce an
encoding of RPO and POLO to the satisfiability of propositional logic
(SAT). We implemented these encodings in our termination tool AProVE.
Extensive experiments have shown that one can obtain speedups in
orders of magnitude by this encoding and the application of modern
SAT solvers.
The talk is based on joint work with Elena Annov, Mike Codish, Carsten Fuhs,
JÃƒÂ¼rgen Giesl, Aart Middeldorp, RenÃƒÂ© Thiemann, and Harald Zankl.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol07401/DagSemProc.07401.5/DagSemProc.07401.5.pdf
Termination
SAT
recursive path order
polynomial interpretation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2007-11-29
7401
1
22
10.4230/DagSemProc.07401.6
article
Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen
Many problems occurring in verification can be reduced to proving
the satisfiability of conjunctions of literals in a background theory.
This can be a concrete theory (e.g. the theory of real or rational numbers),
the extension of a theory with additional functions (free, monotone, or
recursively defined) or a combination of theories. It is therefore very
important to have efficient procedures for checking the satisfiability of
conjunctions of ground literals in such theories.
We present some new results on hierarchical and modular reasoning in
complex theories, as well as several examples of application domains
in which efficient reasoning is possible. We show, in particular,
that various phenomena analyzed in the verification literature can
be explained in a unified way using the notion of local theory extension.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol07401/DagSemProc.07401.6/DagSemProc.07401.6.pdf
Automated reasoning
Combinations of decision procedures
Verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2007-11-29
7401
0
0
10.4230/DagSemProc.07401.7
article
Termination of Programs using Term Rewriting and SAT Solving
Giesl, Jürgen
Schneider-Kamp, Peter
Thiemann, René
Swiderski, Stephan
Nguyen, Manh Thang
De Schreye, Daniel
Serebrenik, Alexander
There are many powerful techniques for automated termination analysis of
term rewrite systems (TRSs). However, up to now they have hardly been used
for real programming languages. In this talk, we describe recent results
which permit the application of existing techniques from term rewriting
in order to prove termination of programs. We discuss two possible approaches:
1. One could translate programs into TRSs and then use existing tools to
verify termination of the resulting TRSs.
2. One could adapt TRS-techniques to the respective programming languages
in order to analyze programs directly.
We present such approaches for the functional language Haskell and the logic
language Prolog. Our results have been implemented in the termination provers
AProVE and Polytool. In order to handle termination problems resulting
from real programs, these provers had to be coupled with modern SAT solvers,
since the automation of the TRS-termination techniques had to
improve significantly. Our resulting termination analyzers are currently
the most powerful ones for Haskell and Prolog.
Termination
Term Rewriting
Haskell
Prolog
SAT Solving