2020-10-20T22:42:26Zhttp://edoc.mpg.de/ac_p_oai.ploai:edoc.mpg.de:2018102010-12-0287:932
Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER
Hillenbrand, Thomas
Dahn, Ingo
Vigneron, Laurent
In the last years, the development of automated theorem
provers has been advancing in a so to speak Olympic spirit,
following the motto "faster, higher, stronger"; and the
{Waldmeister} system has been a part of that endeavour. We
will survey the concepts underlying this prover, which
implements Knuth-Bendix completion in its unfailing variant.
The system architecture is based on a strict separation of
active and passive facts, and is realized via specifically
tailored representations for each of the central data
structures: indexing for the active facts, set-based
compression for the passive facts, successor sets for the
conjectures. In order to cope with large search spaces,
specialized redundancy criteria are employed, and the
empirically gained control knowledge is integrated to ease
the use of the system. We conclude with a discussion of
strengths and weaknesses, and a view of future prospects.
Elsevier
2003
Conference-Paper
http://edoc.mpg.de/201810
Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03, Elsevier, 1-13 (2003)
en
oai:edoc.mpg.de:2018122010-12-0287:932
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
Schmidt, Renate A.
Hustadt, Ullrich
Baader, Franz
In this paper we present a translation principle, called the
\emph{axiomatic translation}, for reducing propositional modal logics
with background theories, including
triangular properties such as transitivity, Euclideanness and
functionality, to decidable logics.
The goal of the axiomatic translation principle is to
find simplified theories, which
capture the inference problems in the original theory, but in a way
that is more amenable to automation and easier to deal with by existing
theorem provers.
The principle of the axiomatic translation is conceptually very simple
and can be largely automated.
Soundness is automatic under reasonable assumptions, and termination of
ordered resolution is easily achieved, but
the non-trivial part of the approach is proving completeness.
Springer
2003
Conference-Paper
http://edoc.mpg.de/201812
urn:ISBN:3-540-40559-3
Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, Springer, 412-426 (2003)
en
oai:edoc.mpg.de:2018222010-12-0287:932
Universal variables in disconnection tableaux
Letz, Reinhold
Stenz, Gernot
Cialdea Mayer, Marta
Pirri, Fiora
Springer
2003
Conference-Paper
http://edoc.mpg.de/201822
urn:ISBN:3-540-40787-1
Automated reasoning with analytical tableaux and related methods : International Conference, TABLEAUX 2003, Springer, 117-133 (2003)
en
oai:edoc.mpg.de:2018232010-12-0287:932
The New WALDMEISTER Loop at Work
Gaillourdet, Jean-Marie
Hillenbrand, Thomas
Löchner, Bernd
Spies, Hendrik
Baader, Franz
We present recent developments within the theorem prover \textsc{Waldmeister}.
They rely on a novel organization of the underlying saturation-based proof
procedure into a system architecture. As is known, the saturation process tends
to quickly fill the memory available unless preventive measures are employed.
To overcome this problem, our new ``\textsc{Waldmeister} loop'' features a
highly compact representation of the search state, exploiting its inherent
structure. The implementation just being available, the cost and the benefits
of the concept now can exactly be measured. Indeed are our expectations met
concerning the drastic cut-down of memory usage with only moderate overhead of
time.
In addition it has turned out that the revealed structure of the search state
paves the way to an easily implemented parallelization of the prover with
modest communication requirements and rewarding speed-ups. In order to minimize
communication-related latencies, we discuss some variations of the loop to
maximally profit from multiple processors.
Springer
2003
Conference-Paper
http://edoc.mpg.de/201823
Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, Springer, 317-321 (2003)
en
oai:edoc.mpg.de:2018522010-12-0287:932
Software Model Checking with Abstraction Refinement
Podelski, Andreas
Zuck, Lenore
Attie, Paul
Cortesi, Agostino
Mukhopadhyay, Supratik
Springer
2003
Conference-Paper
http://edoc.mpg.de/201852
urn:ISBN:3-540-00348-7
Verification, model checking, and abstract interpretation : 4th International Conference, VMCAI 2003, Springer, 1-13 (2003)
en
oai:edoc.mpg.de:2018532010-12-0287:932
Superposition modulo a Shostak Theory
Ganzinger, Harald
Hillenbrand, Thomas
Waldmann, Uwe
Baader, Franz
We investigate superposition modulo a Shostak theory $T$ in order to
facilitate reasoning in the amalgamation of $T$ and a free
theory~$F$.
%
Free operators occur naturally e.\,g.\ in program verification
problems when abstracting over subroutines. If their behaviour in
addition can be specified axiomatically, much more of the program
semantics can be captured.
%
Combining the Shostak-style components for deciding the clausal
validity problem with the ordering and saturation techniques
developed for equational reasoning, we derive a refutationally
complete calculus on mixed ground clauses which result for example
from CNF transforming arbitrary universally quantified formulae.
%
The calculus works modulo a Shostak theory in the sense that it
operates on canonizer normalforms. For the Shostak solvers that we
study, coherence comes for free: no coherence pairs need to be
considered.
Springer
2003
Conference-Paper
http://edoc.mpg.de/201853
urn:ISBN:3-540-40559-3
Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, Springer, 182-196 (2003)
en
oai:edoc.mpg.de:2018792010-12-0287:932
Orienting rewrite rules with the Knuth-Bendix order
Korovin, Konstantin
Voronkov, Andrei
We consider two decision problems related to the Knuth-Bendix order (KBO). The
first problem is \emph{orientability}: given a system of rewrite rules $R$,
does there exist an instance of KBO which orients every ground instance of
every rewrite rule in $R$. The second problem is whether a given instance of
KBO orients every ground instance of a given rewrite rule. This problem can
also be reformulated as the problem of solving a single ordering constraint for
the KBO. We prove that both problems can be
solved in the time polynomial in the size of the input.
The polynomial-time algorithm for orientability builds upon an algorithm for
solving systems of homogeneous linear inequalities over integers. We show that
the orientability problem is P-complete. The polynomial-time algorithm for
solving a single ordering constraint does not need to solve systems of linear
inequalities and can be run in time $O(n^2)$. Also we show that if a system is
orientable using a real-valued instance of KBO, then it is also orientable
using an integer-valued instance of KBO. Therefore, all our results hold both
for the integer-valued and the real-valued KBO.
2003
Article
http://edoc.mpg.de/201879
Information and Computation, v.183, 165-186 (2003)
en
oai:edoc.mpg.de:2018832010-12-0287:932
Deciding the Guarded Fragments by Resolution
de Nivelle, Hans
de Rijke, Maarten
We give resolution based decision procedures for both
the strictly guarded fragment and the loosely guarded
fragment of first-order logic. We prove that the
decision procedures are in 2EXPTIME, which is theoretically
optimal.
2003
Article
http://edoc.mpg.de/201883
urn:ISSN:0747-7171
Journal of Symbolic Computation, v.35, 21-58 (2003)
en
oai:edoc.mpg.de:2018862010-12-0287:932
Deciding Modal Logics through Relational Translations into GF2
de Nivelle, Hans
Demri, Stéphane
Areces, Carlos
Blackburn, Patrick
We provide a simple translation from the satisfiability problem for
regular grammar logics with converse into {GF2}, the intersection
of the guarded fragment and the 2-variable fragment of first-order
logic. The translation is theoretically interesting because
it translates modal logics with certain frame conditions into
first-order logic, without explicitly expressing the frame
conditions. Using the same method, one can show that other
modal logics can be naturally translated into {GF2},
including nominal tense logics and intuitionistic propositional
logic. In our view, the results in this paper provide strong
evidence that the natural first-order fragment corresponding
to modal logics, is {GF2}.
Loria
2003
Conference-Paper
http://edoc.mpg.de/201886
Proceedings of the 3rd Methods for Modalities Workshop, Loria, 15-30 (2003)
en
oai:edoc.mpg.de:2018942010-12-0287:932
On Using Ground Joinable Equations in Equational Theorem Proving
Avenhaus, Jürgen
Hillenbrand, Thomas
Löchner, Bernd
When rewriting and completion techniques are used for equational
theorem proving, the axiom set is saturated with the aim to get a
rewrite system that is terminating and confluent on ground terms.
To reduce the computational effort it should (1) be powerful for
rewriting and (2) create not too many critical pairs. These problems
become especially important if some operators are associative and
commutative (\AC). We show in this paper how these two goals can be
reached to some extent by using ground joinable equations for
simplification purposes and omitting them from the generation of new
facts.
%
For the special case of \AC-operators we present a simple redundancy
criterion which is easy to implement, efficient, and effective in
practice, leading to significant speed-ups.
2003
Article
http://edoc.mpg.de/201894
urn:ISSN:0747-7171
Journal of Symbolic Computation, v.36, 217-233 (2003)
en
oai:edoc.mpg.de:2018972010-12-0287:932
AC-compatible Knuth-Bendix Order
Korovin, Konstantin
Voronkov, Andrei
Baader, Franz
We introduce a family of AC-compatible Knuth-Bendix simplification orderings
which are AC-total on ground terms.
Our orderings preserve attractive features of
the original Knuth-Bendix orderings
such as polynomial algorithm for comparing terms; the orderings admit
computationally efficient approximations
like checking weights of terms;
and prefer light terms to heavy ones.
This makes them especially suited for automated deduction
where efficient treatment of orderings is desirable.
Springer
2003
Conference-Paper
http://edoc.mpg.de/201897
Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, Springer, 47-59 (2003)
en
oai:edoc.mpg.de:2018992010-12-0287:932
Representation Theorems and the Semantics of Non-classical Logics, and Applications to Automated Theorem Proving
Sofronie-Stokkermans, Viorica
Fitting, Melvin
Orlowska, Ewa
We give a uniform presentation of representation and
decidability results related to the Kripke-style
semantics of several non-classical logics.
We show that a general representation theorem
(which has as particular instances the representation
theorems as algebras of sets for Boolean algebras,
distributive lattices and semilattices)
extends in a natural way to several classes of operators
and allows to establish a relationship between algebraic
and Kripke-style models. We illustrate the ideas on several examples.
We conclude by showing how the Kripke-style models thus obtained can be used
(if first-order axiomatizable) for automated theorem proving by
resolution for some non-classical logics.
Springer
Copyright Springer Verlag.
2003
InBook
http://edoc.mpg.de/201899
urn:ISBN:3-7908-1541-1
Beyond Two: Theory and Applications of Multiple Valued Logic, 59-100 (2003)
en
oai:edoc.mpg.de:2019032010-12-0287:932
Orienting Equalities with the Knuth-Bendix Order
Korovin, Konstantin
Voronkov, Andrei
Kolaitis, Phokion
Orientability of systems of equalities is the following
problem: given a system of equalities $s_1 \eql t_1, \ldots,
s_n \eql t_n$, does there exist a simplification ordering $\succ$
which orients the system,
that is for every $i \in \{1,...,n\}$,
either $s_i \succ t_i$ or $t_i \succ s_i$.
This problem can be used in rewriting for finding
a canonical rewrite system for a system of equalities
and in theorem proving for adjusting simplification
orderings during completion. We prove that (rather surprisingly)
the problem can be solved in polynomial time when we restrict ourselves to the
Knuth-Bendix orderings.
IEEE
2003
Conference-Paper
http://edoc.mpg.de/201903
18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), IEEE, 75-84 (2003)
en
oai:edoc.mpg.de:2019092010-12-0287:932
Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
Sofronie-Stokkermans, Viorica
We establish a link between the satisfiability of universal
sentences with respect to classes of distributive lattices
with operators and their satisfiability with respect to
certain classes of relational structures.
This justifies a method for structure-preserving translation
to clause form of universal sentences in such classes of
algebras.
We show that refinements of resolution yield decision procedures
for the universal theory of some such classes. In particular, we
obtain exponential space and time decision procedures
for the universal clause theory of
(i) the class of all bounded distributive lattices with
operators satisfying a set of (generalized) residuation
conditions,
(ii) the class of all bounded distributive lattices with
operators,
and a doubly-exponential time decision procedure for the
universal clause theory of the class of all Heyting algebras.
Copyright Elsevier Publishers
2003
Article
http://edoc.mpg.de/201909
urn:ISSN:0747-7171
Journal of Symbolic Computation, v.36, 891-924 (2003)
en
oai:edoc.mpg.de:2019822010-12-0287:932
Boolean and Cartesian Abstraction for Model Checking C Programs
Podelski, Andreas
Ball, Tom
Rajamani, Sriram K.
2003
Article
http://edoc.mpg.de/201982
urn:ISSN:1433-2779
International Journal on Software Tools for Technology Transfer (STTT), v.5, 1-15 (2003)
en
oai:edoc.mpg.de:2019832010-12-0287:932
Verification of Cryptographic Protocols: Tagging Enforces Termination
Blanchet, Bruno
Podelski, Andreas
Gordon, Andrew D.
Springer
2003
Conference-Paper
http://edoc.mpg.de/201983
urn:ISBN:3-540-00897-7
Foundations of software science and computation structures : 6th International Conference, FOSSACS 2003, Springer, 136-152 (2003)
en
oai:edoc.mpg.de:2020192010-12-0287:932
New Directions in Instantiation-Based Theorem Proving
Ganzinger, Harald
Korovin, Konstantin
Kolaitis, Phokion
We consider instantiation-based theorem proving whereby
instances of clauses are generated by certain inferences, and where
inconsistency is detected by propositional tests.
We give a model construction proof of completeness by which restrictive
inference
systems as well as admissible simplification techniques can be
justified. Another contribution of the paper are novel inference
systems that allow one to also employ decision procedures for
first-order fragments more complex than propositional logic.
The decision procedure provides for an approximative consistency test, and the
instance generation inference system is a means of
successively refining the approximation.
IEEE
2003
Conference-Paper
http://edoc.mpg.de/202019
urn:ISBN:0-7695-1884-2
18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), IEEE, 55-64 (2003)
en
oai:edoc.mpg.de:2020212010-12-0287:932
Solving Existentially Quantified Constraints with One Equality and Arbitrarily Many Inequalities
Ratschan, Stefan
Rossi, Francesca
This paper contains the first algorithm that can solve disjunctions of
constraints of
the form $\exists\SVec{y}\STI B \; [ f=0 \;\wedge\; g_1\geq
0\wedge\dots\wedge g_k\geq 0
]$ in free variables $\SVec{x}$, terminating for all cases when this results
in a numerically
well-posed problem. Here the only assumption on the terms $f, g_1,\dots, g_n$
is the
existence of a pruning function, as given by the usual constraint propagation
algorithms
or by interval evaluation. The paper discusses the application of an
implementation of
the resulting algorithm on problems from control engineering, parameter
estimation, and computational geometry.
Springer
2003
Conference-Paper
http://edoc.mpg.de/202021
Principles and practice on constraint programming - CP 2003 : 9th International Conference, CP 2003, Springer, 615-633 (2003)
en
oai:edoc.mpg.de:2020232010-12-0287:932
Probabilistic Classifiers and the Concepts they Recognize
Jaeger, Manfred
Fawcett, Tom
Mishra, Nina
We investigate algebraic, logical, and geometric
properties of concepts recognized by various classes
of probabilistic classifiers. For this we introduce a
natural hierarchy of probabilistic classifiers, the
lowest level of which comprises the naive Bayesian
classifiers. We show that the expressivity of classifiers on the
different levels in the hierarchy is characterized
algebraically by separability with polynomials of
different degrees. A consequence of this result is that
every linearly separable concept can be recognized by a
naive Bayesian classifier. We contrast this result with
negative results about the naive Bayesian classifier
previously reported in the literature, and point out that
these results only pertain to specific learning
scenarios for naive Bayesian classifiers. We also present
some logical and geometric characterizations of linearly
separable concepts, thus providing additional intuitive
insight into what concepts are recognizable by naive
Bayesian classifiers.
AAAI Press
2003
Conference-Paper
http://edoc.mpg.de/202023
urn:ISBN:0-1-57735-189-4
Proceedings of the Twentieth International Conference on Machine Learning (ICML-03), AAAI Press, 266-273 (2003)
en
oai:edoc.mpg.de:2020262010-12-0287:932
A Representation Theorem and Applications
Jaeger, Manfred
Nielsen, Thomas D.
Zhang, Nevin L.
We introduce a set of transformations on the set of all probability
distributions over a finite state space, and show that these
transformations are the only ones that preserve certain
elementary probabilistic relationships. This result provides
a new perspective on a variety of probabilistic inference
problems in which invariance considerations play a role.
Two particular applications we consider in this paper
are the development of an equivariance-based approach to
the problem of measure selection, and a new justification for
Haldane's prior as the distribution that encodes prior
ignorance about the parameter of a multinomial distribution.
Springer
2003
Conference-Paper
http://edoc.mpg.de/202026
urn:ISBN:3-540-40494-5
Symbolic and Quantitative Approaches to Reasoning with Uncertainty :
7th European Conference, ECSQARU 2003, Springer, 50-61 (2003)
en
oai:edoc.mpg.de:2020272010-12-0287:932
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
Ganzinger, Harald
Stuber, Jürgen
Baader, Franz
The paper describes a superposition calculus where quantifiers are eliminated
lazily. Superposition and simplification inferences may employ equivalences
that have arbitrary formulas at their smaller side. A closely related calculus
is implemented in the Saturate system and has shown useful on many examples, in
particular in set theory. The paper presents a completeness proof and reports
on practical experience obtained with the Saturate system.
Springer
2003
Conference-Paper
http://edoc.mpg.de/202027
urn:ISBN:3-540-40559-3
Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, Springer, 335-349 (2003)
en
oai:edoc.mpg.de:2020292010-12-0287:932
Implementing the clausal normal form transformation with proof generation
de Nivelle, Hans
Konev, Boris
Schmidt, Renate
We explain how to implement the clausal normal form transformation
with proof generation. We present
a convenient data structure for sequent calculus proofs, which
will be used for representing the generated proofs.
The data structure allows easy proof checking and generation
of proofs. In addition, it allows
convenient implementation of proof normalization, which is necessary
in order to keep the size of the generated proofs acceptable.
University of Liverpool, University of Manchester
2003
Conference-Paper
http://edoc.mpg.de/202029
Fourth Workshop on the Implementation of Logics, University of Liverpool, University of Manchester, 69-83 (2003)
en
oai:edoc.mpg.de:2020302010-12-0287:932
Automated theorem proving by resolution in non-classical logics
Sofronie-Stokkermans, Viorica
Nadif, Mohamed
Napoli, Amedeo
SanJuan, Eric
Sigayret, Alain
We present several classes of non-classical logics
(many of which are practically relevant in knowledge
representation)
which can be translated into tractable and relatively
simple fragments of classical logic.
In this context, refinements of resolution can be often
used successfully for automated theorem proving, and
in many cases yield optimal decision procedures.
INRIA
2003
Conference-Paper
http://edoc.mpg.de/202030
urn:ISBN:2-7261-1256-0
Fourth International Conference Journees de l'Informatique Messine: Knowledge Discovery and Discrete Mathematics (JIM-03), INRIA, 151-167 (2003)
en
oai:edoc.mpg.de:2020312010-12-0287:932
Model checking mobile ambients
Charatonik, Witold
Dal Zilio, Silvano
Gordon, Andrew Donald
Mukhopadhyay, Supratik
Talbot, Jean-Marc
We settle the complexity bounds of the model checking problem for the ambient
calculus with public names against the ambient logic. We show that if either
the calculus contains replication or the logic contains the guarantee operator,
the problem is undecidable. In the case of the replication-free calculus and
guarantee-free logic we prove that the problem is PSPACE-complete. For the
complexity upper-bound, we devise a new representation of processes that
remains of polynomial size during process execution; this allows us to keep the
model checking procedure in polynomial space. Moreover, we prove
PSPACE-hardness of the problem for several quite simple fragments of the
calculus and the logic; this suggests that there are no interesting fragments
with polynomial-time model checking algorithms.
2003
Article
http://edoc.mpg.de/202031
urn:ISSN:0304-3975
Theoretical Computer Science, v.308, 277-331 (2003)
en
oai:edoc.mpg.de:2020322010-12-0287:932
Subsumption of Concepts in FL_0 for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACE-complete
Kazakov, Yevgeny
de Nivelle, Hans
Calvanese, Diego
De Giacomo, Giuseppe
Franconi, Enrico
We close the gap in the complexity classification of subsumption in the simple
description logic ${\cal FL}_0$, which allows for
conjunctions and universal value restriction only. We prove that the
subsumption problem in ${\cal FL}_0$ is PSPACE-complete for descriptive
semantics when cyclic definitions are allowed. Our proof uses automata theory
and as a by-product we establish the PSPACE-completeness of a certain decision
problem for regular
languages.
CEUR
2003
Conference-Paper
http://edoc.mpg.de/202032
urn:ISSN:1613-0073
2003 International Workshop on Description Logics (DL-03), CEUR, 56-64 (2003)
en
oai:edoc.mpg.de:2020452010-12-0287:932
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
de Nivelle, Hans
Baader, Franz
We present a way of transforming a resolution proof containing
Skolemization into a natural deduction proof of the same formula
but not using Skolemization. The size of the
proof increases only moderately (polynomially).
This makes it possible to translate the output of a resolution
theorem prover into a purely first-order proof that is moderate
in size.
Springer
2003
Conference-Paper
http://edoc.mpg.de/202045
urn:ISBN:3-540-40559-3
Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, Springer, 365-379 (2003)
en
oai:edoc.mpg.de:2020482010-12-0287:932
Compositional Circular Assume-Guarantee Rules Cannot Be Sound and Complete
Maier, Patrick
Gordon, Andrew D.
Circular assume-guarantee reasoning is used for the compositional verification
of concurrent systems. Its soundness has been studied in depth, perhaps because
circularity makes it anything but obvious. In this paper, we investigate
completeness. We show that compositional circular assume-guarantee rules cannot
be both sound and complete.
Springer
2003
Conference-Paper
http://edoc.mpg.de/202048
urn:ISBN:3-540-00897-7
Foundations of software science and computation structures : 6th International Conference, FOSSACS 2003, Springer, 343-357 (2003)
en
oai:edoc.mpg.de:2020522010-12-0287:932
Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II)
Waldmann, Uwe
Cancellative superposition is a refutationally complete
calculus for first-order equational theorem proving in the
presence of the axioms of cancellative abelian monoids, and,
optionally, the torsion-freeness axioms. Thanks to strengthened
ordering restrictions, cancellative superposition avoids some
of the inefficiencies of classical AC-superposition calculi.
We show how the efficiency of cancellative superposition can
be further improved by using variable elimination techniques,
leading to a significant reduction of the number of variable
overlaps. In particular, we demonstrate that in divisible
torsion-free abelian groups, variable overlaps, AC-unification
and AC-orderings can be avoided completely.
2002
Article
http://edoc.mpg.de/202052
urn:ISSN:0747-7171
Journal of Symbolic Computation, v.33, 831-861 (2002)
en
oai:edoc.mpg.de:2020902010-12-0287:932
Finite-Control Mobile Ambients
Charatonik, Witold
Gordon, Andrew Donald
Talbot, Jean-Marc
Le Métayer, Daniel
We define a finite-control fragment of the ambient calculus, a
formalism for describing distributed and mobile computations. A
series of examples demonstrates the expressiveness of our fragment. In
particular, we encode the choice-free, finite-control, synchronous
$\pi$-calculus. We present an algorithm for model checking this fragment
against the ambient logic (without composition adjunct). This is the first
proposal of a model checking algorithm for ambients to deal with
recursively-defined, possibly nonterminating, processes. Moreover, we show
that the problem is PSPACE-complete, like other fragments considered in the
literature. Finite-control versions of other process calculi are obtained via
various syntactic restrictions. Instead, we rely on a novel type system that
bounds the number of active ambients and outputs in a process; any typable
process has only a finite number of derivatives.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202090
urn:ISBN:3-540-43363-5
Programming languages and systems: 11th European Symposium on Programming, ESOP 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Springer, 295-313 (2002)
en
oai:edoc.mpg.de:2021012010-12-0287:932
Shostak Light
Ganzinger, Harald
Voronkov, Andrei
We represent the essential ingredients of Shostak's procedure at a high level
of abstraction, and as a refinement of the Nelson-Oppen procedure. We analyze
completeness issues of the method based on a general notion of theories. We
also formalize a notion of sigma-models and show that on the basis of Shostak's
procedure we cannot distinguish a theory from its approximation represented by
the class of its sigma-models.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202101
urn:ISBN:3-540-43931-5
Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, Springer, 332-346 (2002)
en
oai:edoc.mpg.de:2021022010-12-0287:932
Context trees
Ganzinger, Harald
Nieuwenhuis, Robert
Nivela, Pilar
Goré, Rajeev
Leitsch, Alexander
Nipkow, Tobias
Indexing data structures are well-known to be crucial for the
efficiency of the current state-of-the-art theorem provers.
Examples are \emph{discrimination trees}, which are like tries
where terms are seen as strings and common prefixes are shared,
and \emph{substitution trees}, where terms keep their tree
structure and all common \emph{contexts} can be shared.
Here we describe a new indexing data structure, \emph{context
trees}, where, by means of a limited kind of context variables,
also common subterms can be shared, even if they occur below
different function symbols.
Apart from introducing the concept, we also provide evidence
for its practical value. We describe an implementation of context
trees based on Curry terms and on an extension of substitution
trees with equality constraints and where one does not
distinguish between \emph{internal} and \emph{external}
variables. Experiments with matching show that our preliminary
implementation is already competitive with tightly coded current
state-of-the-art implementations of the other main techniques.
In particular space consumption of context trees
is substantially less than for other index structures.
Springer
2001
Conference-Paper
http://edoc.mpg.de/202102
urn:ISBN:3-540-42254-4
Automated reasoning : First International Joint Conference, IJCAR 2001, Springer, 242-256 (2001)
en
oai:edoc.mpg.de:2021032010-12-0287:932
Extraction of Proofs from the Clausal Normal Form Transformation
de Nivelle, Hans
Bradfield, Julian
We give techniques for extracting proofs from the
Clausal Normal Form transformation. We discuss and solve three
technical problems:
{\bf (1)}. How to handle the introduction of definitions and Skolem functions.
{\bf (2)}. How to generate short (linear size) proofs.
{\bf (3)}. How to handle optimized Skolemization. We reduce it
to standard Skolemization.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202103
urn:ISBN:3-540-44240-5
Computer Science Logic : 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Springer, 584-598 (2002)
en
oai:edoc.mpg.de:2021072010-12-0287:932
Probababilistic Decision Graphs - Combining Verification and AI Techniques for Probabilistic Inference
Jaeger, Manfred
We adopt probabilistic decision graphs developed in the
field of automated verification as a tool for probabilistic model
representation and inference.
We show that probabilistic inference has linear time complexity in
the size of the probabilistic decision graph, that the smallest
probabilistic decision graph for a given distribution is at most
as large as the smallest junction tree for the same distribution,
and that in some cases it can in fact be much smaller.
Behind these very promising features of probabilistic decision graphs
lies the fact that they integrate into a single coherent framework
a number of representational
and algorithmic optimizations
developed for Bayesian networks (use of hidden variables, context-specific
independence, structured representation of conditional probability tables).
Computer Science Department, University of Castilla - La Mancha
2002
Conference-Paper
http://edoc.mpg.de/202107
Proceedings of the First European Workshop on Probabilistic Graphical Models, Computer Science Department, University of Castilla - La Mancha, 81-88 (2002)
en
oai:edoc.mpg.de:2021082010-12-0287:932
Is Logic Effective for Analyzing C Programs?
Hillenbrand, Thomas
Podelski, Andreas
Topić, Dalibor
Charatonik, Witold
Ganzinger, Harald
Max-Planck-Institut für Informatik
2002
Conference-Paper
http://edoc.mpg.de/202108
Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, Max-Planck-Institut für Informatik, 27-30 (2002)
en
oai:edoc.mpg.de:2021092010-12-0287:932
The Next WALDMEISTER Loop
Hillenbrand, Thomas
Löchner, Bernd
Voronkov, Andrei
In saturation-based theorem provers, the reasoning process consists
in constructing the closure of an axiom set under inferences. As is
well-known, this process tends to quickly fill the memory available
unless preventive measures are employed. For implementations based
on the DISCOUNT loop, the passive facts are responsible for most
of the memory consumption. We present a refinement of that loop
allowing such a compression that the space needed for the passive
facts is linearly bound by the number of active facts. In practice,
this will reduce memory consumption in the WALDMEISTER system by
more than one order of magnitude as compared to previous compression
schemes.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202109
urn:ISBN:3-540-43931-5
Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, Springer, 486-500 (2002)
en
oai:edoc.mpg.de:2021102010-12-0287:932
Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems
Ganzinger, Harald
Williams, Denise A.
In this paper we compare three approaches
to polynomial time decidability
for uniform word problems for quasi-varieties.
Two of the approaches,
by Evans and Burris, respectively, are semantical, referring to
certain embeddability and axiomatizability properties.
The third approach is proof-theoretic in nature,
inspired by McAllester's concept of local inference.
We define two closely related notions of locality for equational Horn theories
and show that both the criteria by Evans and Burris lie in between
these two concepts.
In particular, our notion of weak locality subsumes
both Evans' and Burris' method.
IEEE
2001
Conference-Paper
http://edoc.mpg.de/202110
urn:ISBN:0-7695-1281-x
Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS-01), IEEE, 81-90 (2001)
en
oai:edoc.mpg.de:2021152010-12-0287:932
Resolution in modal, description and hybrid logic
Areces, Carlos
de Rijke, Maarten
de Nivelle, Hans
2001
Article
http://edoc.mpg.de/202115
urn:ISSN:0955-792X
Journal of Logic and Computation, v.11, 717-736 (2001)
en
oai:edoc.mpg.de:2021192010-12-0287:932
Compositional Termination Analysis of Symbolic Forward Analysis
Charatonik, Witold
Mukhopadhyay, Supratik
Podelski, Andreas
Cortesi, Agostino
Existing model checking tools for infinite state systems, such as
UPPAAL, HYTECH and KRONOS, use symbolic forward analysis, a possibly
nonterminating procedure. We give termination criteria that allow us to
reason compositionally about systems defined with asynchronous parallel
composition; we can prove the termination of symbolic forward analysis for a
composed system from the syntactic conditions satisfied by the component
systems.
Our results apply to nonlinear hybrid systems; in particular to
rectangular hybrid systems, timed automata and o-minimal systems. In the case
of integer-valued systems we give negative results: forward analysis is not
well-suited for this class of inite-state systems.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202119
urn:ISBN:3-540-43631-6
Verification, Model Checking, and Abstract Interpretation. Third International Workshop, VMCAI 2002, Springer, 109-125 (2002)
en
oai:edoc.mpg.de:2021202010-12-0287:932
On Name Generation and Set-Based Analysis in the Dolev-Yao Model
Charatonik, Witold
Amadio, Roberto
Brim, Lubos
Jancar, Petr
Kretinsky, Mojomir
Kucera, Antonin
We study the control reachability problem in the Dolev-Yao model of
cryptographic protocols when principals are represented by tail recursive
processes with generated names. We propose a conservative approximation of the
problem by reduction to a non-standard collapsed operational semantics and we
introduce checkable syntactic conditions entailing the equivalence of the
standard and the collapsed semantics. Then we introduce a conservative and
decidable set-based analysis of the collapsed operational semantics and we
characterize a situation where the analysis is exact.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202120
urn:ISBN:3-540-44043-7
CONCUR 2002 - Concurrency Theory. 13th International Conference, Springer, 499-514 (2002)
en
oai:edoc.mpg.de:2021212010-12-0287:932
Automated Proof Construction in Type Theory using Resolution
Bezem, Marc
Hendriks, Dimitri
de Nivelle, Hans
We provide techniques to integrate resolution logic with equality
in type theory. The results may be rendered as follows:
{\bf (1)}. A clausification procedure in type theory, equipped with
a correctness proof, all encoded using higher-order primitive recursion.
{\bf (2)}. A novel representation of clauses in minimal logic
such that the $ \lambda $-representation of resolution steps
is linear in the size of the premisses.
{\bf (3)}. Availability of the power of resolution theorem provers in
interactive proof construction systems based on
type theory.
2002
Article
http://edoc.mpg.de/202121
urn:ISSN:0168-7433
Journal of Automated Reasoning, v.29, 253-275 (2002)
en
oai:edoc.mpg.de:2021222010-12-0287:932
Logical Frameworks
Basin, David A.
Matthews, Sean
Gabbay, Dov
Guenthner, Franz
Reidel
2002
InBook
http://edoc.mpg.de/202122
urn:ISBN:1-4020-0699-3
Handbook of Philosophical Logic, 89-164 (2002)
en
oai:edoc.mpg.de:2021232010-12-0287:932
Automated Complexity Analysis Based on Ordered Resolution
Basin, David A.
Ganzinger, Harald
We define order locality
to be a property of clauses relative
to a term ordering. This property is a kind of
generalization of the subformula property for proofs where
the terms appearing in proofs can be bounded,
under the given ordering,
by terms appearing in the goal clause. We show that when a clause set is
order local, then the complexity of its ground entailment problem is
a function of its structure (e.g., full versus Horn clauses),
and the ordering used. We prove that, in many cases, order locality
is equivalent to a clause set being saturated
under ordered resolution. This provides a means of using standard
resolution theorem provers for testing order locality and
transforming non-local clause sets into local ones.
We have used the Saturate system to automatically establish complexity
bounds for a number of nontrivial entailment problems
relative to complexity classes which include polynomial and
exponential time and co-NP.
2001
Article
http://edoc.mpg.de/202123
Journal of the ACM, v.48, 70-109 (2001)
en
oai:edoc.mpg.de:2021272010-12-0287:932
Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP
Charatonik, Witold
Mukhopadhyay, Supratik
Podelski, Andreas
Stuckey, Peter J.
Forward analysis procedures for infinite-state systems such as timed systems
were limited to safety properties. We give the first constraint-based forward
analysis for infinite-state systems that goes beyond safety properties. Namely,
we take the restriction of the $\mu$-calculus to least-fixpoint formulas where
negation is applied to closed subformulas only. We characterize these
properties as perfect models of constraint logic programs, and we present a
tabulation procedure for the top-down evaluation of stratified constraint logic
programs.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202127
urn:ISBN:3-540-43930-7
Logic Programming. 18th International Conference, ICLP 2002, Springer, 115-129 (2002)
en
oai:edoc.mpg.de:2021332010-12-0287:932
Atomic Set Constraints with Projection
Charatonik, Witold
Talbot, Jean-Marc
Tison, Sophie
We investigate a class of set constraints defined as atomic set
constraints augmented with projection. This class subsumes some
already studied classes such as atomic set constraints with
left-hand side projection and INES constraints. All these classes
enjoy a nice property that satisfiability can be performed in cubic time. This
has be contrasted with several other classes of set constraints, such as
definite set constraints and positive set constraints, for which
satisfiability ranges from DEXPTIME-complete to NEXPTIME-complete. However,
these latter classes allow set operators such as intersection or union which
is not the case for the class studied here. In the case of atomic set
constraints with projection one might expect that satisfiability remains
polynomial. Unfortunately, we show that that the satisfiability problem for
this class is no longer polynomial, but CoNP-hard. Furthermore, we devise a
PSPACE algorithm to solve this satisfiability problem.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202133
urn:ISBN:3-540-43916
Rewriting Techniques and Applications. 13th International Conference, RTA 2002, Springer, 311-325 (2002)
en
oai:edoc.mpg.de:2021342010-12-0287:932
Set Constraints with Intersection
Charatonik, Witold
Podelski, Andreas
Set constraints are inclusions between expressions denoting sets of
trees (over a given alphabet of constructor symbols). The
efficiency of their satisfiability test is a central issue in
set-based program analysis, their main application domain. We
introduce the class of {\em set constraints with intersection}\/
(the only operators forming the expressions are constructors and
intersection) and show that its satisfiability problem is
DEXPTIME-complete. This is the first class of set constraints (over
a general constructor alphabet) that falls into this complexity
class. The solved form in our algorithm represents the least
solution as a tree automaton and exhibits which variables denote the
empty set. We furthermore prove that set constraints with
intersection are equivalent to {\em definite set constraints}\/ (in
expressive power, and the satisfiability problems are linearly
inter-reducible). The class of definite set constraints was the
first one for which the decidability question was solved; we hereby
settle also the complexity question.
2002
Article
http://edoc.mpg.de/202134
urn:ISSN:0890-5401
Information and Computation, v.179, 213-229 (2002)
en
oai:edoc.mpg.de:2021362010-12-0287:932
Deduction
Furbach, Ulrich
Ganzinger, Harald
Hasegawa, Ryuzo
Kapur, Deepak
IBFI
2000
Proceedings
http://edoc.mpg.de/202136
urn:ISSN:0940-1121
en
oai:edoc.mpg.de:2021372010-12-0287:932
0/1 Optimization and 0/1 Primal Separation are Equivalent
Eisenbrand, Friedrich
Rinaldi, Giovanni
Ventura, Paolo
ACM SIAM
2002
Conference-Paper
http://edoc.mpg.de/202137
Proceedings of the 13th Annual ACM SIAM Symposium on Discrete Algorithms, ACM SIAM, 920-926 (2002)
en
oai:edoc.mpg.de:2021382010-12-0287:932
A Theory of Inductive Query Answering
de Raedt, Luc
Jaeger, Manfred
Lee, Sau Dan
Mannila, Heikki
We introduce the boolean inductive query evaluation problem, which is
concerned with answering inductive que
ries
that are arbitrary boolean expressions over monotonic and anti-monotonic
predicates. Secondly, we develop a d
ecomposition theory for inductive query evaluation in which
a boolean query $Q$ is reformulated into $k$ sub-queries $Q_i = Q_A \wedge Q_M$
that are the conjunction of a
monotonic and an anti-monotonic predicate.
The solution to each sub-query can be represented using a version space.
We investigate how the number of version spaces $k$ needed to answer the query
can be minimized.
Thirdly, for the pattern domain of strings, we show how the version spaces can
be represented using a novel
data structure, called the version space tree, and can be computed using a
variant of the famous Apriori alg
orithm.
Finally, we present some experiments that validate the approach.
IEEE
2002
Conference-Paper
http://edoc.mpg.de/202138
urn:ISBN:0-7695-1754-4
Proceedings of the 2002 IEEE International Conference on Data Mining (ICDM'02), IEEE, 123-130 (2002)
en
oai:edoc.mpg.de:2021392010-12-0287:932
Proceedings of the 2nd International Workshop on the Implementation of Logics
de Nivelle, Hans
Schulz, Stephan
Max-Planck-Institut für Informatik
2001
Proceedings
http://edoc.mpg.de/202139
urn:ISSN:0946-011X
en
oai:edoc.mpg.de:2021402010-12-0287:932
Logical Algorithms
Ganzinger, Harald
McAllester, David
Stuckey, Peter J.
It is widely accepted that many algorithms can be concisely and clearly
expressed as logical inference rules. However, logic programming has been
inappropriate for the study of the running time of algorithms because there has
not been a clear and precise model of the run time of a logic program. We
present a logic programming model of computation appropriate for the study of
the run time of a wide variety of algorithms.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202140
urn:ISBN:3-540-43930-7
Logic Programming. 18th International Conference, ICLP 2002, Springer, 209-223 (2002)
en
oai:edoc.mpg.de:2021412010-12-0287:932
A new meta-complexity theorem for bottom-up logic programs
Ganzinger, Harald
McAllester, David
Goré, Rajeev
Leitsch, Alexander
Nipkow, Tobias
Nontrivial
meta-complexity theorems, proved once for a programming language
as a whole, facilitate the presentation and analysis
of particular algorithms. This paper gives a new
meta-complexity theorem
for bottom-up logic programs
that is both more general and more accurate
than previous such theorems.
The new theorem applies to algorithms
not handled by previous meta-complexity theorems,
greatly facilitating their analysis.
Springer
2001
Conference-Paper
http://edoc.mpg.de/202141
urn:ISBN:3-540-42254-4
Automated reasoning : First International Joint Conference, IJCAR 2001, Springer, 514-528 (2001)
en
oai:edoc.mpg.de:2021422010-12-0287:932
A Resolution-Based Decision Procedure for Extensions of K4
Ganzinger, Harald
Hustadt, Ullrich
Meyer, Christoph
Schmidt, Renate A.
Zakharyaschev, Michael
Segerberg, Krister
de Rijke, Maarten
Wansing, Heinrich
This paper presents a resolution decision procedure for transitive
propositional modal logics.
The procedure combines the
relational translation method with an
ordered chaining
calculus designed to avoid unnecessary
inferences with transitive relations.
We show the logics K4, KD4 and S4
can be transformed into a bounded class of well-structured clauses
closed under ordered resolution and negative chaining.
CSLI
2001
InBook
http://edoc.mpg.de/202142
urn:ISBN:1-57586-272-7
en
oai:edoc.mpg.de:2021432010-12-0287:932
Efficient deductive methods for program analysis
Ganzinger, Harald
2001
Article
http://edoc.mpg.de/202143
urn:ISSN:0362-1340
ACM SIGPLAN Notices, v.36, 102-103 (2001)
en
oai:edoc.mpg.de:2021442010-12-0287:932
A Phytography of WALDMEISTER
Löchner, Bernd
Hillenbrand, Thomas
The architecture of the {Waldmeister} prover for unit equational
deduction is based on a strict separation of active and passive
facts. After an inspection of the system's proof procedure, the
representation of each of the central data structures is outlined,
namely indexing for the active facts, compression for the passive
facts, successor sets for the hypotheses, and minimal recording of
inference steps for the proof object. In order to cope with large
search spaces, specialized redundancy criteria are employed, and the
empirically gained control knowledge is integrated to ease the use
of the system. The paper concludes with a quantitative comparison of
the {Waldmeister} versions over the years, and a view of the future
prospects.
2002
Article
http://edoc.mpg.de/202144
urn:ISSN:0921-7126
AI Communications, v.15, 127-133 (2002)
en
oai:edoc.mpg.de:2021452010-12-0287:932
Utilitarian Desires
Lang, Jérôme
van der Torre, Leendert W. N.
Weydert, Emil
2002
Article
http://edoc.mpg.de/202145
urn:ISSN:1387-2532
Autonomous Agents and Multi-Agent Systems, v.5, 329-363 (2002)
en
oai:edoc.mpg.de:2021462010-12-0287:932
Recursive resolution for modal logic
Kazakov, Yevgeny
Charatonik, Witold
Ganzinger, Harald
Resolution for the first order logic can be considered as a
practical tool for obtaining a decision procedures for some
theories (cf. \cite{arm}). For modal logics, however, there is
no uniform formulation of the resolution principle, yet the normal modal
logics are the most probable candidates to be decidable
theories. The translational methods for modal logic, treated for
instance in \cite{ohl}, yet possess some uniformness property, but does not
let one to extract proofs from the refutations. On the other hand,
direct methods (cf. \cite{far}, \cite{abadi}) are local which
gives not much practical use of them. This paper presents some
arguments on generalization of the classical propositional resolution
method to the language of modal logic. We give a resolution calculus
for modal logic $\K$ that inherits some features of classical resolution
and propose some suggestions of how can it be used for other modal logics.
Max-Planck-Institut für Informatik
2002
Conference-Paper
http://edoc.mpg.de/202146
Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, Max-Planck-Institut für Informatik, 11-15 (2002)
en
oai:edoc.mpg.de:2021472010-12-0287:932
Constraints and Theorem Proving
Ganzinger, Harald
Nieuwenhuis, Robert
Comon, Hubert
Marché, Claude
Treinen, Ralf
This paper is a tutorial on methods
for first-order theorem proving with constraints.
Springer
2001
Conference-Paper
http://edoc.mpg.de/202147
urn:ISBN:3-540-41950-0
Contraints in Computational Logics, International Summer School (CCL-99), Springer, 159-201 (2001)
en
oai:edoc.mpg.de:2021562010-12-0287:932
A Framework for Circular Assume-Guarantee Rules
Maier, Patrick
Charatonik, Witold
Ganzinger, Harald
Max-Planck-Institut für Informatik
2002
Conference-Paper
http://edoc.mpg.de/202156
Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, Max-Planck-Institut für Informatik, 55-58 (2002)
en
oai:edoc.mpg.de:2021602010-12-0287:932
The undecidability of the first-order theories of one step rewriting in linear canonical systems
Vorobyov, Sergei
2002
Article
http://edoc.mpg.de/202160
Information and Computation, v.175, 182-213 (2002)
en
oai:edoc.mpg.de:2021612010-12-0287:932
On uniform word problems involving bridging operators on distributive lattices
Sofronie-Stokkermans, Viorica
Egly, Uwe
Fermüller, Christian
In this paper we analyze some fragments of the universal theory
of distributive lattices with many sorted bridging operators.
Our interest in such algebras
is motivated by the fact that, in description logics,
numerical features are often expressed by using maps that
associate numerical values to sets (more generally,
to lattice elements).
We first establish a link between satisfiability
of universal sentences
with respect to algebraic models and satisfiability with respect to
certain classes of relational structures.
We use these results for giving a method for
translation to clause form of universal sentences,
and provide some decidability results based on the use of
resolution or hyperresolution.
Links between hyperresolution and tableau methods are also
discussed, and a tableau procedure for checking satisfiability
of formulae of type $t_1 \leq t_2$ is obtained by using a
hyperresolution calculus.
Springer
Copyright Springer Verlag
2002
Conference-Paper
http://edoc.mpg.de/202161
urn:ISBN:3-540-43929-3
Automated Reasoning with Analytic and Related Methods : International Conference, TABLEAUX 2002, Springer, 235-250 (2002)
en
oai:edoc.mpg.de:2021622010-12-0287:932
Relative Completeness of Abstraction Refinement for Software Model Checking
Podelski, Andreas
Ball, Tom
Rajamani, Sriram K.
Kaoen, Joost-Pieter
Stevens, Perdita
Springer
2002
Conference-Paper
http://edoc.mpg.de/202162
urn:ISBN:3-540-43419-4
Tools and algorithms for the construction and analysis of systems : 8th International Conference, TACAS 2002, Springer, 158-172 (2002)
en
oai:edoc.mpg.de:2021632010-12-0287:932
An Algebraic Framework for Abstract Model Checking
Mukhopadhyay, Supratik
Podelski, Andreas
Koenig, Sven
Holte, Robert C.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202163
urn:ISBN:3-540-43941-2
Abstraction, reformulation, and approximation : 5th International Symposium, SARA 2002, Springer, 152-169 (2002)
en
oai:edoc.mpg.de:2021652010-12-0287:932
Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I)
Waldmann, Uwe
We present superposition calculi in which the axioms
of cancellative abelian monoids and, optionally, the
torsion-freeness axiom are integrated. Cancellative
abelian monoids comprise abelian groups, but also such
ubiquitous structures as the natural numbers or multisets.
Our calculi require neither extended clauses nor explicit
inferences with the theory axioms. Compared with
AC-superposition calculi, the number of variable overlaps
is significantly reduced by strong ordering restrictions.
2002
Article
http://edoc.mpg.de/202165
urn:ISSN:0747-7171
Journal of Symbolic Computation, v.33, 777-829 (2002)
en
oai:edoc.mpg.de:2021662010-12-0287:932
A New Input Technique for Accented Letters in Alphabetical Scripts
Waldmann, Uwe
SITMO is a new input technique for accented and special
letters of the Latin alphabet (or other alphabets of comparable
size), which combines in a uniform way short key sequences for
frequently used characters with an easily memorizable scheme to
enter rarely used characters. Compared with traditional modifier
techniques, SITMO requires less additional keys and allows
to access more characters, while for most European languages,
the average number of keystrokes per derived letter is similar
(that is, close to 2).
The Unicode Consortium
2002
Conference-Paper
http://edoc.mpg.de/202166
Proceedings of the 20th International Unicode Conference, The Unicode Consortium (2002)
en
oai:edoc.mpg.de:2021672010-12-0287:932
$\forall\exists^5$-equational theory of context unification is undecidable
Vorobyov, Sergei
2002
Article
http://edoc.mpg.de/202167
Theoretical Computer Science, v.275, 463-479 (2002)
en
oai:edoc.mpg.de:2021692010-12-0287:932
An Algorithm for Isolating the Real Solutions of Semi-algebraic Systems
Xia, Bican
Yang, Lu
2002
Article
http://edoc.mpg.de/202169
Journal of Symbolic Computation, v.34, 461-477 (2002)
en
oai:edoc.mpg.de:2021702010-12-0287:932
SPASS Version 2.0
Weidenbach, Christoph
Brahm, Uwe
Hillenbrand, Thomas
Keen, Enno
Theobalt, Christian
Topić, Dalibor
Voronkov, Andrei
SPASS is an automated theorem prover for full first-order logic with equality.
This system description provides an overview of recent developments in SPASS
2.0, including among others an implementation of contextual rewriting,
refinements of the clause normal form transformation, and enhancements of the
inference engine.
Springer
2002
Conference-Paper
http://edoc.mpg.de/202170
urn:ISBN:3-540-43931-5
Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, Springer, 275-279 (2002)
en
oai:edoc.mpg.de:2312422010-12-0287:932
Logic Programming Infrastructure for Inferences on FrameNet
Baumgartner, Peter
Burchardt, Aljoscha
Alferes, José
Leite, João
Springer
2004
Conference-Paper
http://edoc.mpg.de/231242
urn:ISBN:3-540-23242-7
Logics in artificial intelligence : 9th European Conference, JELIA 2004, Springer, 591-603 (2004)
en
oai:edoc.mpg.de:2312432010-12-0287:932
Darwin: A Theorem Prover for the Model Evolution Calculus
Baumgartner, Peter
Fuchs, Alexander
Tinelli, Cesare
Schulz, Stephan
Tammet, Tanel
Sutcliffe, Geoff
UCC
2004
Conference-Paper
http://edoc.mpg.de/231243
Proceedings of the 1st Workshop on Empirically Successful First Order Reasoning (ESFOR'04), UCC, 1-24 (2004)
en
oai:edoc.mpg.de:2312442010-12-0287:932
Model Based Deduction for Database Schema Reasoning
Baumgartner, Peter
Furbach, Ulrich
Gross-Hardt, Margret
Kleemann, Thomas
Biundo, Susanne
Frühwirth, Thom
Palm, Günther
We aim to demonstrate that automated deduction techniques, in particular those
following the model computation paradigm, are very well suited for database
schema/query reasoning. Specifically, we present an approach to compute
completed paths for database or XPath queries. The database schema and a query
are transformed to disjunctive logic programs with default negation, using a
description logic as an intermediate language. Our underlying deduction system,
KRHyper, then detects if a query is satisfiable or not. In case of a
satisfiable query, all completed paths – those that fulfill all given
constraints – are returned as part of the computed models.
The purpose of computing completed paths is to reduce the workload on a query
processor. Without the path completion, a usual XPath query processor would
search the whole database for solutions to the query, which need not be the
case when using completed paths instead.
We understand this paper as a first step, that covers a basic schema/query
reasoning task by model-based deduction. Due to the underlying expressive logic
formalism we expect our approach to easily adapt to more sophisticated problem
settings, like type hierarchies as they evolve within the XML world.
Springer
2004
Conference-Paper
http://edoc.mpg.de/231244
urn:ISBN:3-540-23166-8
KI 2004: Advances in Artificial Intelligence: 27th Annual German Conference on AI, KI 2004, Springer, 168-182 (2004)
en
oai:edoc.mpg.de:2312452010-12-0287:932
Living Book -- Deduction, Slicing, and Interaction
Baumgartner, Peter
Furbach, Ulrich
Gross-Hardt, Margret
Sinner, Alex
2004
Article
http://edoc.mpg.de/231245
Journal of Automated Reasoning, v.32, 259-286 (2004)
en
oai:edoc.mpg.de:2312462010-12-0287:932
In2Math - Interaktive Mathematik- und Informatikgrundausbildung
Baumgartner, Peter
Grabowski, Barbara
Oevel, Walter
Melis, Erica
2004
Article
http://edoc.mpg.de/231246
urn:ISSN:0720-8928
Softwaretechnik-Trends, v.24, 36-45 (2004)
de
oai:edoc.mpg.de:2312472010-12-0287:932
Improving Stable Models Based Planning by Bidirectional Search
Baumgartner, Peter
Mediratta, Anupam
Sasikumar, M.
Vakil, R.
Kavitha, M.
ALLIED
2004
Conference-Paper
http://edoc.mpg.de/231247
urn:ISBN:81-7764-711-3
Proceedings of the 5th International Conference on Knowledge Based Computer Systems (KBCS 2004), ALLIED, 404-413 (2004)
en
oai:edoc.mpg.de:2312482010-12-0287:932
Conformant Planning via Heuristic Forward Search: A New Approach
Brafman, Ronen
Hoffmann, Jörg
Zilberstein, Shlomo
Koehler, Jana
Koenig, Sven
AAAI
2004
Conference-Paper
http://edoc.mpg.de/231248
urn:ISBN:1-57735-200-9
Proceedings of the Fourteenth International Conference on Automated Planning and Scheduling (ICAPS 2004), AAAI, 355-364 (2004)
en
oai:edoc.mpg.de:2312492010-12-0287:932
L'atelier FOCAL
Dubois, Catherine
Jaume, Mathieu
Pons, Olivier
Prevosto, Virgile
Juilland, Jacques
Université de Franche-Comté
2004
Conference-Paper
http://edoc.mpg.de/231249
Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2004), Université de Franche-Comté, 321-324 (2004)
fr
oai:edoc.mpg.de:2312502010-12-0287:932
DPLL(T): Fast Decision Procedures
Ganzinger, Harald
Hagen, George
Nieuwenhuis, Robert
Oliveras, Albert
Tinelli, Cesare
Alur, Rajeev
Peled, Doron
Springer
2004
Conference-Paper
http://edoc.mpg.de/231250
urn:ISBN:3-540-22342-8
Computer aided verification : 16th International Conference, CAV 2004, Springer, 175-188 (2004)
en
oai:edoc.mpg.de:2312512010-12-0287:932
Integration of equational reasoning into instantiation-based theorem proving
Ganzinger, Harald
Korovin, Konstantin
Marcinkowski, Jerzy
Tarlecki, Andrzej
In this paper we present a method for integrating equational reasoning into
instantiation-based theorem proving. The method employs a satisfiability solver
for ground equational clauses together with an instance generation process
based on an ordered paramodulation type calculus for literals. The completeness
of the procedure is proved using the the model generation technique, which
allows us to justify redundancy elimination based on appropriate orderings.
Springer
2004
Conference-Paper
http://edoc.mpg.de/231251
urn:ISBN:3-540-23024-6
Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL, Springer, 71-84 (2004)
en
oai:edoc.mpg.de:2312522010-12-0287:932
Fast Term Indexing with Coded Context Trees
Ganzinger, Harald
Nieuwenhuis, Robert
Nivela, Pilar
Indexing data structures have a crucial impact on
the performance of automated theorem provers. Examples are discrimination
trees, which are like tries where terms are seen as strings and common prefixes
are shared, and substitution trees, where terms keep their tree structure and
all common contexts can be shared. Here we describe a new indexing data
structure, called context trees, where, by means of a limited kind of context
variables, also common subterms can be shared, even if they occur below
different function symbols. Apart from introducing the concept, we also provide
evidence for its practical value. We show how context trees can be implemented
by means of abstract machine instructions. Experiments with matching benchmarks
show that our implementation is competitive with tightly coded current
state-of-the-art implementations of the other main techniques. In particular
space consumption of context trees is significantly less than for other index
structures.
2004
Article
http://edoc.mpg.de/231252
Journal of Automated Reasoning, v.32, 103-120 (2004)
en
oai:edoc.mpg.de:2312532010-12-0287:932
Modular Proof Systems for Partial Functions with Weak Equality
Ganzinger, Harald
Sofronie-Stokkermans, Viorica
Waldmann, Uwe
Basin, David
Rusinowitch, Michael
The paper presents a modular superposition calculus for the
combination of first-order theories involving both total
and partial functions. Modularity means that inferences are
pure, only involving clauses over the alphabet of either
one, but not both, of the theories. The calculus is shown
to be complete provided that functions that are not in the
intersection of the component signatures are declared as
partial. This result also means that if the
unsatisfiability of a goal modulo the combined theory does
not depend on the totality of the functions in the
extensions, the inconsistency will be effectively found.
Moreover, we consider a constraint superposition calculus
for the case of hierarchical theories and show that it has
a related modularity property. Finally we identify cases
where the partial models can always be made total so that
modular superposition is also complete with respect to the
standard (total function) semantics of the theories.
Springer
2004
Conference-Paper
http://edoc.mpg.de/231253
urn:ISBN:3-540-22345-2
Automated reasoning : Second International Joint Conference, IJCAR 2004, Springer, 168-182 (2004)
en
oai:edoc.mpg.de:2312542010-12-0287:932
SCAN is complete for all {Sahlqvist} formulae
Goranko, Valentin
Hustadt, Ullrich
Schmidt, Renate A.
Vakarelov, Dimiter
Berghammer, Rudolf
Möller, Bernhard
Struth, Georg
SCAN is an algorithm for reducing monadic existential second-order logic
formulae to equivalent simpler formulae, often first-order logic
formulae. It is provably impossible for such a reduction to first-order
logic to be always successful, even if there is an equivalent
first-order formula for a second-order logic formula. In this paper we
show that SCAN successfully computes the first-order equivalents of all
Sahlqvist formulae in the classical (multi-)modal language.
Springer
2004
Conference-Paper
http://edoc.mpg.de/231254
urn:ISBN:3-540-22145-X
Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Springer, 149-162 (2004)
en
oai:edoc.mpg.de:2312552010-12-0287:932
Ordered Landmarks in Planning
Hoffmann, Jörg
Porteous, Julie
Sebastia, Laura
2004
Article
http://edoc.mpg.de/231255
urn:ISSN:1076-9757
Journal of Artificial Intelligence Research, v.22, 215-278 (2004)
en
oai:edoc.mpg.de:2312562010-12-0287:932
Set Computation for Nonlinear Control
Jaulin, Luc
Ratschan, Stefan
Hardouin, Laurent
2004
Article
http://edoc.mpg.de/231256
Reliable Computing, v.10, 1-26 (2004)
en
oai:edoc.mpg.de:2312572010-12-0287:932
Tools and algorithms for the construction and analysis of systems : 10th International Conference, TACAS 2004 ; held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004
Jensen, Kurt
Podelski, Andreas
Springer
2004
Proceedings
http://edoc.mpg.de/231257
urn:ISBN:3-540-21299
en
oai:edoc.mpg.de:2312582010-12-0287:932
A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment
Kazakov, Yevgeny
Alferes, José Júlio
Leite, João
We consider a two-variable guarded fragment with number restrictions for binary
relations and give a satisfiability preserving transformation of formulas in
this fragment to the three-variable guarded fragment. The translation can be
computed in polynomial time and produces a formula that is linear in the size
of the initial formula even for the binary coding of number restrictions. This
allows one to reduce reasoning problems for many description logics to the
satisfiability problem for the guarded fragment.
Springer
© Springer-Verlag
2004
Conference-Paper
http://edoc.mpg.de/231258
urn:ISBN:3-540-23242-7
Logics in artificial intelligence : 9th European Conference, JELIA 2004, Springer, 372-384 (2004)
en
oai:edoc.mpg.de:2312592010-12-0287:932
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards
Kazakov, Yevgeny
de Nivelle, Hans
Basin, David
Rusinowitch, Michael
We show how well-known refinements of ordered resolution, in particular
redundancy elimination and ordering constraints in combination with a selection
function, can be used to obtain a decision procedure for the guarded fragment
with transitive guards. Another contribution of the paper is a special scheme
notation, that allows to describe saturation strategies and show their
correctness in a concise form.
Springer
© Springer-Verlag
2004
Conference-Paper
http://edoc.mpg.de/231259
urn:ISBN:3-540-22345-2
Automated reasoning : Second International Joint Conference, IJCAR 2004, Springer, 122-136 (2004)
en
oai:edoc.mpg.de:2312602010-12-0287:932
Intuitionistic LTL and a New Characterization of Safety and Liveness
Maier, Patrick
Marcinkowski, Jerzy
Tarlecki, Andrzej
Classical linear-time temporal logic (LTL) is capable of specifying of and
reasoning about infinite behaviors only. While this is appropriate for
specifying non-terminating reactive systems, there are situations (e.g.
assume-guarantee reasoning, run-time verification) when it is desirable to be
able to reason about finite and infinite behaviors. We propose an
interpretation of the operators of LTL on finite and infinite behaviors, which
defines an intuitionistic temporal logic (ILTL). We compare the expressive
power of LTL and ILTL. We demonstrate that ILTL is suitable for
assume-guarantee reasoning and for expressing properties that relate finite and
infinite behaviors. In particular, ILTL admits an elegant logical
characterization of safety and liveness properties.
Springer
2004
Conference-Paper
http://edoc.mpg.de/231260
Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL, Springer, 295-309 (2004)
en
oai:edoc.mpg.de:2312612010-12-0287:932
Introduction to the Special Issue on Verification and Computational Logic
Podelski, Andreas
2004
Article
http://edoc.mpg.de/231261
urn:ISSN:1471-0684
Theory and Practice of Logic Programming (TPLP), v.4 (2004)
en
oai:edoc.mpg.de:2312622010-12-0287:932
Transition Invariants
Podelski, Andreas
Rybalchenko, Andrey
IEEE
2004
Conference-Paper
http://edoc.mpg.de/231262
urn:ISBN:0-7695-2192-4
Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS 2004, IEEE, 32-41 (2004)
en
oai:edoc.mpg.de:2312632010-12-0287:932
A Complete Method for the Synthesis of Linear Ranking Functions
Podelski, Andreas
Rybalchenko, Andrey
Levi, Giorgio
Steffen, Bernhard
Springer
2004
Conference-Paper
http://edoc.mpg.de/231263
urn:ISBN:3-540-20803-8
Verification, model checking, and abstract interpretation : 5th International Conference, VMCAI 2004, Springer, 239-251 (2004)
en
oai:edoc.mpg.de:2312642010-12-0287:932
Convergent Approximate Solving of First-order Constraints by Approximate Quantifiers
Ratschan, Stefan
2004
Article
http://edoc.mpg.de/231264
ACM Transactions on Computational Logic, v.5, 264-281 (2004)
en
oai:edoc.mpg.de:2312652010-12-0287:932
Robust Pole Clustering of Parametric Uncertain Systems Using Interval Methods
Ratschan, Stefan
Vehi, Josep
Bittanti, Sergio
In this paper a new methodology to solve the pole clustering problem for
parametric
uncertain systems is introduced: The problem of clustering the closed loop
poles into
prescribed D-regions in the complex plane is stated as a quantified
constraint problem
that represents bounded uncertain parameters by intervals; and an
engineering-oriented
approach based on interval methods is developed to solve this quantified
constraint
problem. The result is a new, robust, reliable and
design oriented method to deal with parametric uncertain systems.
The methodology presented in this paper allows to find a good
controller that places the closed loop poles in the desired
location in the complex plane. In case there is no solution, the
method allows also to "tune" the problem, either enlarging the pole
locations or reducing the uncertainty domain.
The approach presented in this paper can be used either for linear
or non-linear systems and for any kind of parametric bounded
uncertainty.
Several simple examples illustrate the uses, limits and scope of
the methodology.
Publ. for the International Federation of Automatic Control by Elsevier
2004
Conference-Paper
http://edoc.mpg.de/231265
urn:ISBN:0-08-044012-6
Robust control design 2003 : (ROCOND 2003) ; a proceedings volume from the 4th IFAC symposium, Publ. for the International Federation of Automatic Control by Elsevier, 323-328 (2004)
en
oai:edoc.mpg.de:2312662010-12-0287:932
Two Proof Systems for Peirce Algebras
Schmidt, Renate A.
Or{\l}owska, Ewa
Hustadt, Ullrich
Berghammer, Rudolf
Möller, Bernhard
Struth, Georg
This paper develops and compares two tableaux-style proof systems for
Peirce algebras.
One is a tableau refutation proof system, the other is a proof system in
the style of Rasiowa-Sikorski.
Springer
2004
Conference-Paper
http://edoc.mpg.de/231266
urn:ISBN:3-540-22145-X
Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Springer, 238-251 (2004)
en
oai:edoc.mpg.de:2312672010-12-0287:932
Multi-Agent Dynamic Logics with Informational Test
Schmidt, Renate A.
Tishkovsky, Dmitry
This paper investigates a family of logics for reasoning about the
dynamic activities and informational attitudes of agents,
namely the agents' beliefs and knowledge.
The logics are based
on a new formalisation and semantics
of the test operator of
propositional dynamic logic
and a representation of actions which
distinguishes abstract actions from concrete actions.
The new test operator, called informational test,
can be used to formalise the beliefs and knowledge of particular agents
as dynamic modalities.
This approach is consistent
with the formalisation
of the agents' beliefs and knowledge
as K(D)45 and S5 modalities.
Properties concerning informativeness, truthfulness and
preservation of beliefs
are proved for a derivative of the informational test operator.
It is shown that common belief and common knowledge
can be expressed in the considered logics.
This means,
the logics are more expressive
than propositional dynamic logic with
an extra modality for belief or knowledge.
The logics remain decidable and belong to 2EXPTIME.
Versions of the considered logics express natural additional properties
of beliefs or knowledge and interaction of beliefs or knowledge with
actions.
It is shown that a simulation of PDL can be constructed in one of these
extensions.
2004
Article
http://edoc.mpg.de/231267
urn:ISSN:1012-2443
Annals of Mathematics and Artificial Intelligence, v.42, 5-36 (2004)
en
oai:edoc.mpg.de:2312682010-12-0287:932
Interaction between Knowledge, Action and Commitment within Agent Dynamic Logic
Schmidt, Renate A.
Tishkovsky, Dmitry
Hustadt, Ullrich
This paper considers a new class of agent dynamic logics which
provide a formal means of specifying and reasoning
about the agents' activities and informational, motivational and
practical aspects of the behaviour of the agents. We present a
Hilbert-style deductive system for a basic agent dynamic logic and
consider a number of extensions of this logic with axiom schemata
formalising interactions between knowledge and commitment (expressing an
agent's awareness of her commitments), and interactions between
knowledge and actions (expressing no learning and persistence of
knowledge after actions). The deductive systems are proved sound and
complete with respect to a Kripke-style semantics. Each of the
considered logics is shown to have the small model property and
therefore decidable.
2004
Article
http://edoc.mpg.de/231268
urn:ISSN:0039-3215
Studia Logica, v.78, 381-415 (2004)
en
oai:edoc.mpg.de:2312692010-12-0287:932
Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras
Sofronie-Stokkermans, Viorica
In this paper we give resolution-based decision procedures for
the positive theory of certain finitely-generated varieties of
algebras. The method is based on the existence of
representation theorems for such classes of algebras.
IEEE Computer Society
2004
Conference-Paper
http://edoc.mpg.de/231269
Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL-2004), IEEE Computer Society, 32-37 (2004)
en
oai:edoc.mpg.de:2312702010-12-0287:932
Applying Automatic Planning Systems to Airport Ground Traffic Control -- A Feasibility Study
Trueg, Sebastian
Hoffmann, Jörg
Nebel, Bernhard
Biundo, Susanne
Frühwirth, Thom
Palm, Günther
Springer
2004
Conference-Paper
http://edoc.mpg.de/231270
urn:ISBN:3-540-23166-8
KI 2004: Advances in Artificial Intelligence: 27th Annual German Conference on AI, KI 2004, Springer, 183-197 (2004)
en
oai:edoc.mpg.de:2312712010-12-0287:932
A Superposition View on Nelson-Oppen
Hillenbrand, Thomas
Sattler, Ulrike
CEUR
2004
Conference-Paper
http://edoc.mpg.de/231271
urn:ISSN:1613-0073
Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, CEUR, 16-20 (2004)
en
oai:edoc.mpg.de:2318872010-12-0287:932
Two Proof Systems for Peirce Algebras
Schmidt, Renate A.
Orlowska, Ewa
Hustadt, Ullrich
Berghammer, Rudolf
Möller, Bernhard
Struth, Georg
This paper develops and compares two tableaux-style proof systems for
Peirce algebras.
One is a tableau refutation proof system, the other is a proof system in
the style of Rasiowa-Sikorski.
Springer
2004
Conference-Paper
http://edoc.mpg.de/231887
urn:ISBN:3-540-22145-X
Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Springer, 238-251 (2004)
en
oai:edoc.mpg.de:2318942010-12-0287:932
Intuitionistic LTL and a New Characterization of Safety and Liveness
Maier, Patrick
Marcinkowski, Jerzy
Tarlecki, Andrzej
Classical linear-time temporal logic (LTL) is capable of specifying of and
reasoning about infinite behaviors only. While this is appropriate for
specifying non-terminating reactive systems, there are situations (e.g.
assume-guarantee reasoning, run-time verification) when it is desirable to be
able to reason about finite and infinite behaviors. We propose an
interpretation of the operators of LTL on finite and infinite behaviors, which
defines an intuitionistic temporal logic (ILTL). We compare the expressive
power of LTL and ILTL. We demonstrate that ILTL is suitable for
assume-guarantee reasoning and for expressing properties that relate finite and
infinite behaviors. In particular, ILTL admits an elegant logical
characterization of safety and liveness properties.
Springer
2004
Conference-Paper
http://edoc.mpg.de/231894
Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL, Springer, 295-309 (2004)
en
oai:edoc.mpg.de:2319112010-12-0287:932
L'atelier FOCAL
Dubois, Catherine
Jaume, Mathieu
Pons, Olivier
Prevosto, Virgile
Juilland, Jacques
Université de Franche-Comté
2004
Conference-Paper
http://edoc.mpg.de/231911
Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2004), Université de Franche-Comté, 321-324 (2004)
fr
ResultSet_6Uzp4mzNe7W_range_100-199