Quantifier Elimination and Provers Integration
S. Ghilardi
(Università degli Studi di Milano, Italy)
We exploit quantifier elimination in the global design of combined
decision and semi-decision procedures for theories over non-disjoint
signatures, thus providing in particular extensions of Nelson-Oppen
combination schema.
A Decision Procedure for a Sublanguage of Set Theory
Involving Monotone, Additive, and Multiplicative Functions
D. Cantone
(University of Catania, Italy)
J.T. Schwartz
(New York University, USA)
C.G. Zarba
(Stanford University, USA)
MLSS is a decidable sublanguage of set theory involving the
constructs membership, set equality, set inclusion, union,
intersection, set difference, and singleton.
In this paper we extend MLSS with constructs for expressing
monotonicity, additivity, and multiplicativity properties of set-to-set
functions. We prove that the resulting language is decidable by
reducing the problem of determining the satisfiability of its sentences
to the problem of determining the satisfiability of sentences of MLSS.
Canonicity
N. Dershowitz
(Tel Aviv University, Israel)
We explore how different proof orderings induce different
notions of saturation. We relate completion, paramodulation,
saturation, redundancy elimination, and rewrite system
reduction to proof orderings.
Transforming Equality Logic to Propositional Logic
H. Zantema
(Eindhoven University of Technology, The Netherlands)
J.F. Groote
(Eindhoven University of Technology, The Netherlands)
We investigate and compare various ways of transforming equality
formulas to propositional formulas, in order to be able to solve
satisfiability in equality logic by means of satisfiability in
propositional logic. We propose a new way combining two desirable
properties of earlier methods.
On Leaf Permutative Theories and Occurrence Permutation
Groups
T. Boy de la Tour
(INPG, France)
M. Echenim
(INPG, France)
Leaf permutative theories contain variable-permuting
equations, so that rewriting a term may lead to an exponential
number of terms which are only permutations of it. In [1]
Avenhaus and Plaisted propose to represent such sets by
stratified terms, and to deduce directly with these. Our aim
is to use computational group theory to analyse the complexity
of the corresponding problems, and hopefully devise better
algorithms than [1]. In order to express stratified sets as
orbits, we adopt a representation of terms based on
occurrences, which can conveniently be permuted. An algorithm
solving a basic equivalence problem is presented.
Light-Weight Theorem Proving for Debugging and Verifying
Pointer Manipulating Programs
S. Ranise
(LORIA - INRIA-Lorraine, France)
D. Déharbe
(UFRN - Universidade Federal do Rio Grande do Norte, Brasil)
We describe a combination of BDDs and superposition theorem proving,
called light-weight theorem proving, and its application to the flexible
and efficient automation of the reasoning activity required to debug and
verify pointer manipulating programs. This class of programs is
notoriously challenging to reason about and it is also interesting from
a programming point of view since pointers are an important source of
bugs. The implementation of our technique (in a system called haRVey
scales up significantly better than state-of-the-art tools such as E (a
superposition prover) and Simplify (a prover based on the Nelson and
Oppen combination of decision procedures and used in ESC/Java) on a set
of proof obligations arising in debugging and verifying C functions
manipulating pointers.
Can Decision Procedures be Learnt Automatically?
M. Jamnik
(The University of Cambridge, England)
P. Janicic
(University of Belgrade, Yugoslavia)
In this paper we present an investigation into whether and how
can decision procedures be learnt automatically. Our approach
consists of two stages. First, a refined brute-force search
procedure applies exhaustively a set of given elementary
methods to try to solve a corpus of conjectures generated by a
stochastic context-free grammar. The successful proof traces
are saved. In the second stage, a learning algorithm (by
Jamnik et al.) tries to extract a required supermethod (i.e.,
decision procedure) from the given traces. In the paper, this
technique is applied to elementary methods that encode the
operations of the Fourier-Motzkin's decision procedure for
Presburger arithmetic on rational numbers. The results of our
experiment are encouraging.
Manipulating Tree Tuple Languages by Transforming Logic Programs
S. Limet
(Universitté d'Orléans, France)
G. Salzer
(Technische Universität Wien, Austria)
We introduce inductive definitions over language expressions as a
framework for specifying tree tuple languages. Inductive definitions
and their sub-classes correspond naturally to classes of logic programs,
and operations on tree tuple languages correspond to the transformation
of logic programs. We present an algorithm based on unfolding and
definition introduction that is able to deal with several classes of
tuple languages in a uniform way. Termination proofs for clause classes
translate directly to closure properties of tuple languages, leading to
new decidability and computability results for the latter.
Combining Non-Stably Infinite Theories
C. Tinelli
(The University of Iowa, USA)
C.G. Zarba
(Stanford University, USA)
The Nelson-Oppen combination method combines decision procedures for
first-order theories over disjoint signatures into a single decision
procedure for the union theory. To be correct, the method requires that
the component theories be stably infinite. This restriction makes the
method inapplicable to many interesting theories such as, for instance,
theories having only finite models.
In this paper we provide a new combination method that can combine any
theory that is not stably infinite with another theory, provided that
the latter is what we call a shiny theory. Examples of shiny theories
include the theory of equality, the theory of partial orders, and the
theory of total orders.
An interesting consequence of our results is that any decision procedure
for the satisfiability of quantifier-free Sigma-formulae in a
Sigma-theory T can always be extended to accept inputs over an arbitrary
signature Omega containing Sigma.
Exact Algorithms for MAX-SAT
H. Zhang
(University of Iowa, USA)
H. Shen
(University of Iowa, USA)
F. Manyà
(Universitat de Lleida, Spain)
The maximum satisfiability problem (MAX-SAT) is stated as
follows: Given a Boolean formula in CNF, find a truth
assignment that satisfies the maximum possible number of its
clauses. MAX-SAT is MAX-SNP-complete and received much
attention recently. One of the challenges posed by Alber,
Gramm and Niedermeier in a recent survey paper asks: Can
MAX-SAT be solved in less than $2^n$ ``steps''? Here, $n$ is
the number of different variables in the formula and a step
may take polynomial time of the input. We answered this
challenge positively by showing that a popular algorithm based
on branch-and-bound is bounded by $O(b2^n)$ in time, where $b$
is the maximum number of occurrences of any variable in the
input.
When the input formula is in 2-CNF, that is, each clause has
at most two literals, MAX-SAT becomes MAX-2-SAT and the
decision version of MAX-2-SAT is still NP-complete. The best
bound of the known algorithms for MAX-2-SAT is $O(m2^{m/5})$,
where $m$ is the number of clauses. We propose an efficient
decision algorithm for MAX-2-SAT whose time complexity is
bound by $O(n2^n)$. This result is substantially better than
the previously known results. Experimental results also show
that our algorithm outperforms any algorithm we know on
MAX-2-SAT.
Reachability in Conditional Term Rewriting Systems
G. Feuillade
(ENS Cachan / IRISA, France)
T. Genet
(IRISA / Université de Rennes 1, France)
In this paper, we study the reachability problem for conditional term
rewriting systems. Given two ground terms 's' and 't', our practical
aim is to prove that s cannot be rewritten into t (in any number of
steps) using a join conditional term rewriting system R (possibly not
terminating and not confluent). The proof method we propose relies on
an over approximation of reachable terms for join conditional term
rewriting systems. This approximation is computed using an extension of
the tree automata completion algorithm to the conditional case.
A Resolution-based Model Building Algorithm for a Fragment of OCC1N=
N. Peltier
(CNRS - LEIBNITZ - IMAG, France)
OCC1N is a decidable subclass of first-order clausal logic without
equality. OCC1N becomes undecidable when equational literals are
allowed, but remains decidable if equality is restricted to ground
terms only.
First, we extend this decidability result to some non ground equational
literals. By carefully restricting the use of the equality predicate
we obtain a new decidable class. We show that existing paramodulation
calculi cannot terminate on the considered class and we define a new
simplification rule which allows to ensure termination. Second, we
show that the automatic extraction of Herbrand models is possible from
satisfiable sets in the class. These models are represented by certain
finite sets of (possibly equational and non ground) linear atoms. The
difficult point here is to show that this formalism is suitable as a
model representation mechanism, i.e. that the evaluation of arbitrary
(non equational) first-order formulae in such interpretations is a
decidable problem.