2020-10-19T22:47:00Zhttp://edoc.mpg.de/ac_ft_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: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: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: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:2018982010-12-0287:932
A Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning
Maier, Patrick
We develop an abstract lattice-theoretic framework within which
we study soundness and other properties of circular assume-
guarantee (A-G) rules constrained by side conditions. We
identify a particular side condition, non-blockingness, which
admits an intelligible inductive proof of the soundness of
circular A-G reasoning. Besides, conditional circular rules
based on non-blockingness turn out to be complete in various
senses and stronger than a large class of sound conditional A-G
rules. In this respect, our framework enlightens the foundations
of circular A-G reasoning.
Due to its abstractness, the framework can be instantiated to
many concrete settings. We show several known circular A-G rules
for compositional verification to be instances of our generic
rules. Thus, we do the circularity-breaking inductive argument
once to establish soundness of our generic rules, which then
implies soundness of all the instances without resorting to
technically complicated circularity-breaking arguments for each
single rule. In this respect, our framework unifies many
approaches to circular A-G reasoning and provides a starting
point for the systematic development of new circular A-G rules.
Universität des Saarlandes
2003
PhD-Thesis
http://edoc.mpg.de/201898
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: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: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: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: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: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: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:2312722010-12-0287:932
Instance Generation Methods for Automated Reasoning
Jacobs, Swen
There are several different methods which try to decide unsatisfiability of a
set of clauses by generating an unsatisfiable set of instances of the input
clauses. We consider the \emph{Disconnection Tableau Calculus}, \emph{Primal
Partial Instantiation} and \emph{Resolution-Based Instance-Generation}, all of
which can be seen as refinements of the clause linking approach. We present
these three methods accurately and in a consistent manner. Similarities and
equivalences of the methods will be pointed out and we will show if proofs of
one calculus can be simulated by a different method, generating only instances
from the given proof.
Universität des Saarlandes
2005
Thesis
http://edoc.mpg.de/231272
en
oai:edoc.mpg.de:2319652010-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/231965
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:2319972010-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/231997
urn:ISBN:3-540-23242-7
Logics in artificial intelligence : 9th European Conference, JELIA 2004, Springer, 372-384 (2004)
en
oai:edoc.mpg.de:2320022010-12-0287:932
A Superposition View on Nelson-Oppen
Hillenbrand, Thomas
Sattler, Ulrike
CEUR
2004
Conference-Paper
http://edoc.mpg.de/232002
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:2320322010-12-0287:932
Instance Generation Methods for Automated Reasoning
Jacobs, Swen
There are several different methods which try to decide unsatisfiability of a
set of clauses by generating an unsatisfiable set of instances of the input
clauses. We consider the \emph{Disconnection Tableau Calculus}, \emph{Primal
Partial Instantiation} and \emph{Resolution-Based Instance-Generation}, all of
which can be seen as refinements of the clause linking approach. We present
these three methods accurately and in a consistent manner. Similarities and
equivalences of the methods will be pointed out and we will show if proofs of
one calculus can be simulated by a different method, generating only instances
from the given proof.
Universität des Saarlandes
2004
Thesis
http://edoc.mpg.de/232032
en
oai:edoc.mpg.de:2320342010-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/232034
Journal of Automated Reasoning, v.32, 103-120 (2004)
en
oai:edoc.mpg.de:2378662010-12-0287:932
Summaries for while programs with recursion
Wagner, Silke
Max-Planck-Institut für Informatik
2004
Report
http://edoc.mpg.de/237866
en
oai:edoc.mpg.de:2378702010-12-0287:932
Intuitionistic LTL and a New Characterization of Safety and Liveness
Maier, Patrick
Max-Planck-Institut für Informatik
2004
Report
http://edoc.mpg.de/237870
en
oai:edoc.mpg.de:2378712010-12-0287:932
Resolution decision procedures for the guarded fragment with transitive guards
de Nivelle, Hans
Kazakov, Yevgeny
Max-Planck-Institut für Informatik
2004
Report
http://edoc.mpg.de/237871
en
oai:edoc.mpg.de:2790752010-12-0287:932
An Abstract Model of Routing in Mobile Ad Hoc Networks
Yuan, Cong
Billington, Jonathan
Freiheit, Jörn
DAIMI
2005
Conference-Paper
http://edoc.mpg.de/279075
Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI, 137-156 (2005)
en
oai:edoc.mpg.de:2790882011-05-0587:932
Enhanced Workflow Models as a Tool for Judicial Practitioners
Freiheit, Jörn
Münch, Susanne
Schöttle, Hendrik
Sijanski, Grozdana
Zangl, Fabrice
Meersman, Robert
Tari, Zahir
Herrero, Pilar
Méndez, Gonzalo
Cavedon, Lawrence
Martin, David
Hinze, Annika
Buchanan, George
Pérez, María S.
Robles, Víctor
Humble, Jan
Albani, Antonia
Dietz, Jan L.G.
Panetto, Herve
Scannapieco, Monica
Halpin, Terry
Spyns, Peter
Zaha, Johannes Maria
Zimány, Esteban
Stefanakis, Emmanuel
Dillon, Tharam
Feng, Ling
Jarrar, Mustafa
Lehmann, Jos
de Moor, Aldo
Duval, Erik
Aroyo, Lora
In the past, attempts were made to make law and justice more accessible to
general audience and to legal practitioners using models of legal texts. We
present a new approach to make the judicial workflows easier to understand. By
using process modelling methods, the developed representation emphasises on
improving transparency, on promoting mutual trust and on formalising models for
verification. To design semi-formal models interviews are used as well as legal
texts are consulted. These models are formalised in a second step. The models
are enhanced with hierarchies, modules and the generation of different views.
Language problems are also treated. The subsequent formalised models are used
to verify trigger events and timing of judicial workflows, which have very
specific requirements in terms of periods of time and fixed dates. A new tool,
Lexecute, is presented which gives new perspectives into justice and reveal new
potentials for modelling methods in the field of justice.
Springer
2005
Conference-Paper
http://edoc.mpg.de/279088
urn:ISBN:3-540-29739-1
On the move to meaningful internet systems 2005: OTM 2005 Workshops : OTM Confederated International Workshops and Posters, AWeSOMe, CAMS, GADA, MIOS+INTEROP, ORM, PhDS, SeBGIS, SWWS, and WOSE 2005, Springer, 26-27 (2005)
en
oai:edoc.mpg.de:2791012010-12-0287:932
Integration of a Software Model Checker into Isabelle
Daum, Matthias
Maus, Stefan
Schirmer, Norbert
Seghir, Mohammed Nassim
Sutcliffe, Geoff
Voronkov, Andrei
The paper presents a combination of interactive and automatic tools in the area
of software verification.
We have integrated a newly developed software model checker into an interactive
verification environment for imperative programming languages.
Although the problems in software verification are mostly too hard for full
automation, we could increase the level of automated assistance by discharging
less interesting side conditions.
That allows the verification engineer to focus on the abstract algorithm,
safely assuming unbounded arithmetic and unlimited buffers.
Springer
2005
Conference-Paper
http://edoc.mpg.de/279101
urn:ISBN:3-540-30553-X
Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, Springer, 381-395 (2005)
en
oai:edoc.mpg.de:2791212010-12-0287:932
Comparing Instance Generation Methods for Automated Reasoning
Jacobs, Swen
Waldmann, Uwe
Beckert, Bernhard
The clause linking technique of Lee and Plaisted
proves the unsatisfiability
of a set of first-order clauses
by generating a sufficiently large set of instances of these clauses
that can be shown to be propositionally unsatisfiable.
In recent years,
this approach has been refined in several directions,
leading to both tableau-based methods,
such as the Disconnection Tableau Calculus,
and saturation-based methods,
such as Primal Partial Instantiation
and Resolution-based Instance Generation.
We investigate the relationship between these calculi
and answer the question to what extent
refutation or consistency proofs in one calculus
can be simulated in another one.
Springer
Copyright 2005 Springer-Verlag
2005
Conference-Paper
http://edoc.mpg.de/279121
urn:ISBN:3-540-28931-3
Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX 2005, Springer, 153-168 (2005)
en
oai:edoc.mpg.de:3144872010-12-0287:932
Field Constraint Analysis
Wies, Thomas
Kuncak, Viktor
Lam, Patrick
Podelski, Andreas
Rinard, Martin C.
Emerson, E. Allen
Namjoshi, Kedar S.
We introduce \emph{field constraint analysis}, a new
technique for verifying data structure invariants. A
field constraint for a field is a formula specifying a set of objects
to which the field can point. Field constraints enable
the application of decidable logics to data structures
which were originally beyond the scope of these logics, by verifying the
backbone of the data structure and then verifying
constraints on fields that cross-cut the backbone in
arbitrary ways. Previously, such cross-cutting fields
could only be verified when they were uniquely determined by
the backbone, which significantly limits the range of
analyzable data structures.
Field constraint analysis permits \emph{non-deterministic} field
constraints on cross-cutting fields, which allows the verificiation
of invariants for data structures such as skip lists. Non-deterministic
field constraints also enable the verification of invariants between
data structures, yielding an expressive generalization of static
type declarations.
The generality of our field constraints requires new
techniques, which are orthogonal to the traditional use of
structure simulation. We present one such technique and
prove its soundness. We have implemented this technique
as part of a symbolic shape analysis deployed in
the context of the Hob system for verifying data structure
consistency. Using this implementation we were able to
verify data structures that were previously beyond the
reach of similar techniques.
Springer
2006
Conference-Paper
http://edoc.mpg.de/314487
Verification, Model Checking, and Abstract Interpretation : 7th International Conference, VMCAI 2006, Springer, 157-173 (2006)
en
oai:edoc.mpg.de:3145652011-07-0887:932
Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment
Kazakov, Yevgeny
We apply the framework of Bachmair and Ganzinger for saturation-based theorem
proving to derive a range of decision procedures for logical formalisms,
starting with a simple terminological language EL, which allows for conjunction
and existential restrictions only, and ending with extensions of the guarded
fragment with equality, constants, functionality, number restrictions and
compositional axioms of
form S ◦ T Í H. Our procedures are derived in a uniform way using standard
saturation-based calculi enhanced with simplication rules based on the general
notion of redundancy. We argue that such decision procedures can be applied for
reasoning in expressive description logics, where they have certain advantages
over traditionally used tableau procedures, such as optimal worst-case
complexity and
direct correctness proofs.
Universität des Saarlandes
2006
PhD-Thesis
http://edoc.mpg.de/314565
en
oai:edoc.mpg.de:3146012010-12-0287:932
Abstrakte Übergangsrelationen als Mittel zur Verifikation von Programmeigenschaften
Schäf, Martin
Die Entwicklung von Software ist ein fehleranf¨alliger Prozess. Allein die
Tatsache,
dass ein Programm ausf¨uhrbar ist und dass f¨ur eine begrenzte Menge
von Testf¨allen keine Fehler in der Ausf¨uhrung des Programms auftritt, sagt
nicht aus, dass ein Programm fehlerfrei ist. Vor allem in Bereichen, in denen
Software nicht einfach im Fall eines Versagens abgeschaltet und repariert
werden kann ist es wichtig beweisen zu k¨onnen, dass Software fehlerfrei
ist. Es existieren verschiedene Methoden diesen Beweis zu erbringen. Die
g¨angigste Methode ist deduktive Verifikation, in der die Software von Hand
verifiziert wird. Dieser Vorgang ist allerdings teuer und fehleranf¨allig.
Formale Verifikation ist eine j¨ungere Methode die vor allem f¨ur die
Verifikation
von Hardware verwendet wird. Mit formaler Verifikation k¨onnen
Systeme mit endlicher Zustandsmenge automatisch bewiesen werden. Um
die Methode auf Software anzuwenden, muss diese abstrahiert werden, da
die Zustandsmenge eines Programms unendlich gross sein kann. Das U¨ berpr
¨ufen von Programmeigenschaften auf einem abstrakten Modell wird auch
Model Checking genannt.
Es existieren verschiedene Ans¨atze um durch Model Checking
Programmeigenschaften
zu beweisen. In [esp] wird ein Ansatz vorgestellt tempor¨are
Sicherheitseigenschaften eines Programms automatisch zu Beweisen. [tin]
stellt eine M¨oglichkeit vor durch Model Checking Terminierung und Fairness
zu beweisen.
Diese Ans¨atze arbeiten immer auf dem gesamten Programm. In dieser Arbeit
wird eine Methode hergeleitet, ein Programm oder einen Teil eines Programms
in eine abstrakte U¨ bergangsrelation zu u¨bersetzen und durch diese,
Annahmen ¨uber das Verhalten der Programmvariablen zu beweisen. Der Vorteil
dieser Methode ist die Wiederverwendbarkeit von U¨ bergangsrelationen.
Da diese unabh¨angig vom Kontrollfluss sind, gen¨ugt es, f¨ur einen Programmteil
einmalig die U¨ bergangsrelation zu berechnen, egal wie oft dieser Teil
verwendet
wird. Diese Eigenschaft bietet es an, dieses Verfahren in den Prozess
der Softwareentwicklung einzubeziehen um die Fehlersuche zu erleichtern,
oder Fehler fr¨uhzeitig zu erkennen.
4
Universität des Saarlandes
2006
Thesis
http://edoc.mpg.de/314601
de
oai:edoc.mpg.de:3566252010-12-0287:932
Precise Thread-Modular Verification
Malkis, Alexander
Podelski, Andreas
Rybalchenko, Andrey
Springer
2007
Conference-Paper
http://edoc.mpg.de/356625
urn:ISBN:3-540-74060-0
info:doi/10.1007/978-3-540-74061-2_14
Filé, Gilberto; Riis Nielson, Hanne: Static Analysis : 14th International Symposium, SAS 2007, Springer, 218-232 (2007)
en
oai:edoc.mpg.de:3566262010-12-0287:932
Region Stability Proofs for Hybrid Systems
Podelski, Andreas
Wagner, Silke
We present a method and tool (and implementation) for automatic proofs of
region stability for hybrid systems. The formal basis of our approach is the
new notion of \emph{snapshot sequences}. We use snapshot sequences for a
characterization of region stability. Our abstraction-based algorithm checks
the conditions in this characterization. A number of experiments demonstrate
the practical potential of our approach.
Springer
2007
Conference-Paper
http://edoc.mpg.de/356626
urn:ISBN:3-540-75453-9
info:doi/10.1007/978-3-540-75454-1_23
Raskin, J.-F.; Thiagarajan, P.S.: Formal Modeling and Analysis of Timed Systems : 5th International Conference, FORMATS 2007, Springer, 320-335 (2007)
en
oai:edoc.mpg.de:3566282010-12-0287:932
Theory Instantiation
Ganzinger, Harald
Korovin, Konstantin
Springer
2006
Conference-Paper
http://edoc.mpg.de/356628
urn:ISBN:3-540-48281-4
info:doi/10.1007/11916277_34
Hermann, Miki; Voronkov, Andrei: Logic for Programming, Artificial Intelligence, and Reasoning : 13th International Conference, LPAR 2006, Springer, 497-511 (2006)
en
oai:edoc.mpg.de:3566292010-12-0287:932
Path Invariants
Beyer, Dirk
Henzinger, Thomas
Majumdar, Rupak
Rybalchenko, Andrey
The success of software verification depends on the ability to find a suitable
abstraction of a program automatically. We propose a method for automated
abstraction refinement which overcomes some limitations of current predicate
discovery schemes. In current schemes, the cause of a false alarm is identified
as an infeasible error path, and the abstraction is refined in order to remove
that path. By contrast, we view the cause of a false alarm -the spurious
counterexample- as a full-fledged program, namely, a fragment of the original
program whose control-flow graph may contain loops and represent unbounded
computations. There are two advantages to using such path programs as
counterexamples for abstraction refinement. First, we can bring the whole
machinery of program analysis to bear on path programs, which are typically
small compared to the original program. Specifically, we use constraint-based
invariant generation to automatically infer invariants of path
programs-so-called path invariants. Second, we use path invariants for
abstraction refinement in order to remove not one infeasibility at a time, but
at once all (possibly infinitely many) infeasible error computations that are
represented by a path program. Unlike previous predicate discovery schemes, our
method handles loops without unrolling them; it infers abstractions that
involve universal quantification and naturally incorporates disjunctive
reasoning.
ACM
2007
Conference-Paper
http://edoc.mpg.de/356629
urn:ISBN:978-1-59593-633-2
info:doi/10.1145/1250734.1250769
Ferrante, Jeanne; McKinley, Kathryn S.: PLDI'07 : Proceedings of the 2007 Conference on Programming Language Design and Implementation, ACM, 300-309 (2007)
en
oai:edoc.mpg.de:3566402010-12-0287:932
Proving Thread Termination
Cook, Byron
Podelski, Andreas
Rybalchenko, Andrey
Concurrent programs are often designed such that certain functions executing
within critical threads must terminate. Examples of such cases can be found in
operating systems, web servers, e-mail clients, etc. Unfortunately, no known
automatic program termination prover supports a practical method of proving the
termination of threads. In this paper we describe such a procedure. The
procedure's scalability is achieved through the use of environment models that
abstract away the surrounding threads. The procedure's accuracy is due to a
novel method of incrementally constructing environment abstractions. Our method
finds the conditions that a thread requires of its environment in order to
establish termination by looking at the conditions necessary to prove that
certain paths through the thread represent well-founded relations if executed
in isolation of the other threads. The paper gives a description of
experimental results using an implementation of our procedureon Windows device
drivers and adescription of a previously unknown bug found withthe tool.
ACM
2007
Conference-Paper
http://edoc.mpg.de/356640
urn:ISBN:978-1-59593-633-2
info:doi/10.1145/1250734.1250771
Ferrante, Jeanne; McKinley, Kathryn S.: PLDI'07 : Proceedings of the 2007 Conference on Programming Language Design and Implementation, ACM, 320-330 (2007)
en
oai:edoc.mpg.de:3566772010-12-0287:932
Proving that programs eventually do something good
Cook, Byron
Gotsman, Alexey
Podelski, Andreas
Rybalchenko, Andrey
Vardi, Moshe
ACM
2007
Conference-Paper
http://edoc.mpg.de/356677
urn:ISBN:1-59593-575-4
info:doi/10.1145/1190216.1190257
Hofmann, Martin; Felleisen, Matthias: Conference Record of POPL® 2007 : The 34th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, ACM, 265-276 (2007)
en
oai:edoc.mpg.de:3566782012-01-1087:932
A Method and a Tool for Automatic Verification of Region Stability for Hybrid Systems
Podelski, Andreas
Wagner, Silke
We propose a model checking method and tool that integrates state abstraction
techniques for the automatic proof of a stability property for hybrid systems
called \emph{region stability}. It is based on a new notion of
\emph{snapshots} which yield characteristic discretizations of trajectories.
We have implemented the tool and applied it to solve a number of verification
problems, including the fully automatic stability proof for the break curve
behavior of a train system.
Max-Planck-Institut für Informatik
2007
Report
http://edoc.mpg.de/356678
en
oai:edoc.mpg.de:3567072010-12-0287:932
ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement
Podelski, Andreas
Rybalchenko, Andrey
Software model checking with abstraction refinement is emerging as a practical
approach to verify industrial software systems. Its distinguishing
characteristics lie in the way it applies logical reasoning to deal with
abstraction. It is therefore natural to investigate whether and how the use of
a constraint-based programming language may lead to an elegant and concise
implementation of a practical tool. In this paper we describe the outcome of
our investigation. Using a Prolog system together with Constraint Logic
Programming extensions as the implementation platform of our choice we have
built such a tool, called ARMC (for Abstraction Refinement Model Checking),
which has already been used for practical verification.
Springer
2007
Conference-Paper
http://edoc.mpg.de/356707
urn:ISBN:3-540-69608-3
info:doi/10.1007/978-3-540-69611-7_16
Hanus, Michael: Practical aspects of declarative languages : 9th International Symposium, PADL 2007, Springer, 245-259 (2007)
en
oai:edoc.mpg.de:3567082010-12-0287:932
Invariant Synthesis for Combined Theories
Beyer, Dirk
Henzinger, Thomas
Majumdar, Rupak
Rybalchenko, Andrey
Springer
2007
Conference-Paper
http://edoc.mpg.de/356708
urn:ISBN:978-3-540-69735-0
info:doi/10.1007/978-3-540-69738-1_27
Cook, Byron; Podelski, Andreas: Verification, Model Checking, and Abstract Interpretation : 8th International Conference, VMCAI 2007, Springer, 378-394 (2007)
en
oai:edoc.mpg.de:5194552011-07-0487:932
A Reinterpretation of the Deductive Tableaux System in Higher-Order Logic
Ayari, Abdelwaheb
Our research investigates frameworks supporting the formalization of
programming calculi and their application to deduction-based progr am
synthesis. Here we report on a case study: within a conservative
extension of higher-order logic implemented in the Isabelle system, we
derived rules for program development which can simulate those of the
deductive tableau proposed by Manna and Waldinger. We have used the
resulting theory to synthesize a library of verified programs, focusing
in particular on sorting algorithms. Our experience suggests
that the methodology we propose is well suited both to implement and
use programming calculi, extend them, partially automate them, and
even formally reason about their correctness.
Universität des Saarlandes
1995
Thesis
http://edoc.mpg.de/519455
en
oai:edoc.mpg.de:5195062010-12-0287:932
Relational Bayesian Networks
Jaeger, Manfred
A new method is developed to represent probabilistic relations on
multiple random events. Where previously knowledge bases containing
probabilistic rules were used for this purpose, here a probability
distribution over the relations is directly represented by a
Bayesian network. By using a powerful way of specifying conditional probability
distributions in these networks, the resulting formalism is more
expressive than the previous ones. Particularly, it provides for constraints
on equalities of events, and it allows to define complex, nested
combination functions.
Morgan Kaufmann
1997
Conference-Paper
http://edoc.mpg.de/519506
urn:ISBN:1-55860-485-5
Geiger, Dan; Shenoy, Prakash Pundalik: Proceedings of the 13th Conference of Uncertainty in Artificial Intelligence (UAI-13), Morgan Kaufmann, 266-273 (1997)
en
oai:edoc.mpg.de:5195302011-07-0887:932
Transformations of First-Order Formulae for Automated Reasoning
Rock, Georg
Theorem prover for first-order logic usually operate on a set of clauses.
Since it is more natural and adequate to code problems in full first-order
logic, the problem of translating a formula into clause normal form
is an important one in this field. From experience we know that a theorem
prover can find a
proof more easily with a compact clause normal form than with a huge set of
clauses.
In this thesis we present powerful methods to obtain compact clause normal
forms.
Universität des Saarlandes
1995
Thesis
http://edoc.mpg.de/519530
en
oai:edoc.mpg.de:5195622011-07-0487:932
A Calculus of Simplification for Superposition
Christen, Michael
Universität des Saarlandes
1997
Thesis
http://edoc.mpg.de/519562
en
oai:edoc.mpg.de:5195722011-07-0487:932
Quantifier Elimination in Second-Order Predicate Logic
Engel, Thorsten
Universität des Saarlandes
1996
Thesis
http://edoc.mpg.de/519572
en
oai:edoc.mpg.de:5195792011-07-0887:932
Testing the Satisfiability of RPO Constraints
Timm, Jan-Georg
Universität des Saarlandes
1997
Thesis
http://edoc.mpg.de/519579
en
oai:edoc.mpg.de:5196092011-07-0787:932
Superposition Extended with Sorts
Gaede, Bernd
Sorted problem formulations often result in shorter proofs.
In this thesis, the integration of ordered inference rules and rules for
sort constraints in one calculus and the resulting system architecture
for its implementation SPASS are presented. Thus, SPASS (Synergetic Prover
Augmenting Superposition with Sorted logic) is a theorem-proving program
for first-order logic with equality and sorts.
Universität Kaiserslautern
1995
Thesis
http://edoc.mpg.de/519609
en
oai:edoc.mpg.de:5196102011-05-0687:932
Parallel Unit Resulting Resolution
Meyer, Christoph
The term ``Parallel unit resulting resolution'' refers to a modified unit
resulting resolution rule working on sets
of substitutions. We modified the inference rule in order to investigate term
indexing and to exploit
parallelism in automated reasoning. Term indexing supports the construction of
efficient automated
reasoning systems by providing rapid access to first-order predicate calculus
terms with specific properties.
The theoretical background and the implementation of a theorem prover called
{\sc Purr} which implements
parallel unit resulting resolution as well as experiments with {\sc Purr} are
presented in this thesis. The
author addresses the reader interested in new indexing techniques and in
distributed theorem proving.
Universität des Saarlandes
1996
Thesis
http://edoc.mpg.de/519610
en
oai:edoc.mpg.de:5196122011-07-0487:932
Static analysis of functional programs via Linear Logic
Bach, Alexander
This thesis investigates aspects of the general relationship between simply
typed lambda-calculus and a linear term calculus based on Intuitionistic Linear
Logic. It introduces a notion of minimization on linear lambda-terms that
removes super ous nonlinear operations (storage). Two different embeddings of
the simply typed lambda-calculus into the linear term calculus are studied with
respect to their properties under minimization. We define operational semantics
for both term calculi. In support of Abramsky's thesis, that linear types are
useful in doing abstract interpretation of functional programs, we demonstrate
- using translation together with minimization - a syntactic method to do
strictness analysis on lambda-terms, via the linear typing calculus. This leads
to useful optimizations of call-by-name reduction on lambda-terms.
Universität des Saarlandes
1996
Thesis
http://edoc.mpg.de/519612
en
oai:edoc.mpg.de:5196242011-07-0487:932
Effiziente Subsumption in Deduktionssystemen
Becker, Joachim
Es wurden Datenstrukturen und Algorithmen in der Programmiersprache C
entwickelt, die einen
effizienten Subsumptionstest auf Klauseln für einen Resolutionsbeweiser
ermöglichen. Die benötigten
Datenstrukturen, mit deren Hilfe man den Subsumptionstest von Term- auf
Klauselebene liften kann,
wurden in einer "Black-Box" zum Aufbewahren von Klauseln zusammengefaßt.
Universität des Saarlandes
1994
Thesis
http://edoc.mpg.de/519624
de
oai:edoc.mpg.de:5196342010-12-0287:932
Resolution Theorem Proving
Bachmair, Leo
Ganzinger, Harald
We review the fundamental resolution-based methods for first-order
theorem proving and present them in a uniform
framework. We show that these calculi can
be viewed as specializations of non-clausal resolution with simplification.
Simplification techniques are justified with the help of a rather
general notion of redundancy for inferences.
As simplification and other techniques for the elimination of
redundancy are indispensable for an acceptable behaviour
of any practical theorem prover
this work is the first uniform treatment of resolution-like techniques
in which the avoidance of redundant computations attains the attention
it deserves.
In many cases our presentation of a resolution method will
indicate new ways of how to improve the method
over what was known previously.
We also give
answers to several open problems in the area.
Elsevier
This chapter appeared in the Handbook of Automated Reasoning, North Holland,
2001.
2001
InBook
http://edoc.mpg.de/519634
Handbook of Automated Reasoning, 19-99 (2001)
en
oai:edoc.mpg.de:5196632010-12-0287:932
Measure Selection: Notions of Rationality and Representation Independence
Jaeger, Manfred
We take another look at the general problem of selecting a
preferred probability measure
among those that comply with some given constraints.
The dominant role that entropy maximization has obtained in
this context is questioned by arguing that the minimum information
principle on which it is based could be supplanted by an at least
as plausible ``likelihood of evidence'' principle.
We then review a method for turning given selection functions
into representation independent variants, and discuss the tradeoffs
involved in this transformation.
Morgan Kaufmann
1998
Conference-Paper
http://edoc.mpg.de/519663
Cooper, Gregory S.; Moral, Serafín: Proceedings of the 14th Conference on Uncertainty in Artificial Intelligence (UAI-98), Morgan Kaufmann, 274-281 (1998)
en
oai:edoc.mpg.de:5196642010-12-0287:932
Convergence Results for Relational Bayesian Networks
Jaeger, Manfred
Relational Bayesian networks are an extension of the method of probabilistic
model construction by Bayesian networks. They define probability distributions
on finite relational structures by conditioning the probability of a
ground atom $r(a_1,\ldots,a_n)$\ on first-order properties of
$a_1,\ldots,a_n$\ that have been established by previous random decisions.
In this paper we investigate from a finite model theory perspective
the convergence properties of the distributions defined in this manner.
A subclass of relational Bayesian networks is identified that define
distributions with convergence laws for first-order properties.
IEEE
1998
Conference-Paper
http://edoc.mpg.de/519664
Pratt, Vaughan: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS-98), IEEE, 44-55 (1998)
en
oai:edoc.mpg.de:5196652010-12-0287:932
Reasoning About Infinite Random Structures with Relational Bayesian Networks
Jaeger, Manfred
Relational Bayesian networks extend standard Bayesian networks by
integrating
some of the expressive power of first-order logic into the Bayesian network
paradigm. As in the case of the related technique of knowledge based
model construction, so far, decidable semantics only have been provided
for finite stochastic domains. In this paper we extend the semantics
of relational Bayesian networks, so that they also define probability
distributions over countably infinite structures. Using
a technique remeniscent of quantifier elimination methods in model theory,
we show that
probabilistic queries about these distributions are decidable.
Morgan Kaufmann
1998
Conference-Paper
http://edoc.mpg.de/519665
urn:ISBN:1-55860-554-1
Cohn, Anthony G.; Schubert, Lenhart; Shapiro, Stuart C.: Proceedings of the 6th International Conference on Principles of Knowledge Representation and Reasoning (KR-98), Morgan Kaufmann, 570-581 (1998)
en
oai:edoc.mpg.de:5196742010-12-0287:932
$\forall\exists^\ast$-Equational Theory of Context Unification is $\Pi_1^0$-Hard
Vorobyov, Sergei
\begin{abstract}
Context unification is a particular case of second-order
unification, where all second-order variables are \emph{unary} and
only \emph{linear} functions are sought for as solutions. Its
decidability is an open problem. We present the simplest (currently
known) undecidable quantified fragment of the theory of
\emph{context unification} by showing that for every signature
containing a $\geq\!2$-ary symbol one can construct a \emph{context
equation} ${\mathcal E}\,(p,r,\overline{F},\overline{w})$ with
parameter $p$, first-order variables $r$, $\overline{w}$, and
context variables $\overline{F}$ such that the set of true sentences
of the form
\[\forall r\;\exists\;\overline{F}\;\exists\;\overline{w}\;\;
{\mathcal E}(p,r,\overline{F},\overline{w})\] is $\Pi_1^0$-hard
(i.e., every co-r.e. set is many-one reducible to it), as $p$ ranges
over finite words of a binary alphabet.
Moreover, the existential prefix above contains just 5 context and 3
first-order variables.
\end{abstract}
Springer
1998
Conference-Paper
http://edoc.mpg.de/519674
urn:ISBN:3-540-64827-5
Brim, Lubos; Gruska, Jozef; Zlatuska, Jirí: Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS-98), Springer, 597-606 (1998)
en
oai:edoc.mpg.de:5196752010-12-0287:932
Complexity of Nonrecursive Logic Programs with Complex Values
Vorobyov, Sergei
Voronkov, Andrei
We investigate complexity of the $\success$ problem for logic query
languages with complex values: check whether a query defines a
nonempty set. The $\success$ problem for recursive query languages
with complex values is undecidable, so we study the complexity of
nonrecursive queries. By complex values we understand values such as
trees, finite sets, and multisets. Due to the well-known
correspondence between relational query languages and datalog, our
results can be considered as results about relational query
languages with complex values. The paper gives a complete complexity
classification of the $\success$ problem for nonrecursive logic
programs over trees depending on the underlying signature, presence
of negation, and range restrictedness. We also prove several results
about finite sets and multisets.
ACM
1998
Conference-Paper
http://edoc.mpg.de/519675
urn:ISBN:0-89791-996-3
Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS-98), ACM, 244-253 (1998)
en
oai:edoc.mpg.de:5196772010-12-0287:932
Subtyping Functional+Nonempty Record Types
Vorobyov, Sergei
\begin{abstract}
\emph{Solving systems of subtype constraints} (or \emph{subtype
inequalities}) is in the core of efficient \emph{type
reconstruction} in modern object-oriented languages with subtyping
and inheritance, two problems known \emph{polynomial time
equivalent}. It is important to know how different combinations of
type constructors influence the complexity of the problem.
We show the \emph{NP-hardness} of the satisfiability problem for
subtype inequalities between object types built by using
simultaneously both the functional and the non-empty record type
constructors, but without any atomic types and atomic subtyping.
The class of constraints we address is intermediate with respect to
known classes. For pure functional types with atomic subtyping of a
special non-lattice (\emph{crown}) form solving subtype constraints
is PSPACE-complete \cite{Tiuryn92,Frey97}. On the other hand, if
there are no atomic types and subtyping on them, but the largest
$\top$ type is included, then both pure functional and pure record
(separately) subtype constraints are \emph{polynomial time solvable}
\cite{KozenPalsbergSchwartzbach94,Palsberg95ic}, which is mainly due
to the lattice type structure. We show that combining the functional
and nonempty record constructors yields NP-hardness \emph{without
any atomic subtyping}, and the same is true for just a single type
constant with a nonempty record constructor.
\end{abstract}
Springer
1999
Conference-Paper
http://edoc.mpg.de/519677
urn:ISBN:3-540-65922-6
Gottlob, Georg; Grandjean, Etienne; Seyr, Katrin: Proceedings of the 12th International Workshop on Computer Science Logic (CSL-98), Annual Conference on the EACSL, Springer, 285-297 (1999)
en
oai:edoc.mpg.de:5196932010-12-0287:932
A Superposition Decision Procedure for the Guarded Fragment with Equality
Ganzinger, Harald
de Nivelle, Hans
We give a decision procedure for the
guarded fragment with equality.
The procedure is based on resolution with superposition.
The relevance of the guarded fragment lies in the fact
that many modal logics can be translated into it.
In this way the guarded fragment acts as a framework explaining
some of the nice properties of these modal logics.
By constructing an implementable decision procedure for
the guarded fragments we define an effective procedure
for deciding these modal logics.
It is surprising to see that one does not need any sophisticated
simplification and redundancy elimination method to make superposition
terminate on the class of clauses that is obtained from the clausification
of guarded formulas. Yet the decision procedure obtained
is optimal with regard to time complexity.
IEEE
1999
Conference-Paper
http://edoc.mpg.de/519693
urn:ISBN:0-7695-0158-3
Longo, Giuseppe: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99), IEEE, 295-303 (1999)
en
oai:edoc.mpg.de:5197292010-12-0287:932
A Resolution-Based Decision Procedure for Extensions of K4
Ganzinger, Harald
Hustadt, Ullrich
Meyer, Christoph
Schmidt, Renate A.
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/519729
urn:ISBN:1-57586-272-7
Advances in Modal Logic, Volume 2, 225-246 (2001)
en
oai:edoc.mpg.de:5197482010-12-0287:932
Beyond Region Graphs: Symbolic Forward Analysis of Timed Automata
Mukhopadhyay, Supratik
Podelski, Andreas
Springer
1999
Conference-Paper
http://edoc.mpg.de/519748
urn:ISBN:3-540-66836-5
Ramanujam, R; Raman, V.: Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS-99), Springer, 232-244 (1999)
en
oai:edoc.mpg.de:5197572010-12-0287:932
Fairness, Computable Fairness and Randomness
Jaeger, Manfred
Motivated by the observation that executions of a probabilistic
system almost surely are fair,
we interpret concepts of fairness for nondeterministic
processes as partial descriptions of probabilistic
behavior. We propose computable fairness as a very strong
concept of fairness, attempting to capture all the qualitative
properties of probabilistic behavior that we might reasonably
expect to see in the behavior of a nondeterministic system.
It is shown that computable fairness does describe probabilistic
behavior by proving that runs of a probabilistic system
almost surely are computable fair. We then turn to
the question of how sharp an approximation of randomness is obtained
by computable fairness by discussing
completeness of computable fairness for certain classes of
path properties.
School of Computer Science, University of Birmingham
1999
Conference-Paper
http://edoc.mpg.de/519757
Kwiatkowska, Marta: Proceedings of the 2nd International Workshop on Probabilistic Methods in Verification (PROBMIV-99), School of Computer Science, University of Birmingham, 57-66 (1999)
en
oai:edoc.mpg.de:5197582011-07-0487:932
Relations between Abstract Datatypes modeled as Abstract Datatypes
Baumeister, Hubert
In this thesis we define a framework for the specification
of dynamic behavior of software systems. This framework is
motivated by the state as algebra approach and the
model-oriented language Z. From the state as algebra approach
we use the idea of modeling the environment and the state
components as structures of an institution.
However, in contrast to the state as algebra approach, states in
our framework are modeled by structures from any suitable
institution not only those having of algebras as their
structures.
From Z we use the idea that environment, state spaces and
relations between state spaces are specified using the same logic
and how more complex relations can be constructed from simpler
ones by means of the schema calculus. However, we differ from Z
in that our framework can be instantiated by different
institutions, while the approach of Z can only work because of
the particular logical system used by Z.
Universität des Saarlandes
1999
PhD-Thesis
http://edoc.mpg.de/519758
en
oai:edoc.mpg.de:5197712011-07-0887:932
Superposition Theorem Proving for Commutative Algebraic Theories
Stuber, Jürgen
We develop special superposition calculi for first-order
theorem proving in the theories of abelian groups,
commutative rings, and modules and commutative algebras
over fields or over the ring of integers,
in order to make automated theorem proving in these theories more effective.
The calculi are refutationally complete
on arbitrary sets of ground clauses,
which in particular may contain additional function symbols.
The calculi are derived systematically from a representation
of the theory as a convergent term rewriting system.
Compared to standard superposition they have stronger ordering restrictions
so that inferences are applied only to maximal summands,
and they contain macro inference rules
that use theory axioms in a goal directed fashion.
In general we need additional inferences to handle critical peaks
between extended clauses.
We show that these are not needed for abelian groups and modules,
and that for commutative rings and commutative algebras
one such inference suffices for any pair of ground clauses.
To facilitate the construction of term orderings for such calculi
we introduce theory path orderings.
Universität des Saarlandes
2000
PhD-Thesis
http://edoc.mpg.de/519771
en
oai:edoc.mpg.de:5197722010-12-0287:932
Constraint Database Models Characterizing Timed Bisimilarity
Mukhopadhyay, Supratik
Podelski, Andreas
The problem of deciding timed bisimilarity has received increasing attention;
it is important for verification of timed systems. Using a characterization of
timed bisimilarity in terms of models of constraint databases, we present to
our knowledge, the first \emph{local}, \emph{symbolic algorithm} for deciding
timed bisimilarity; previous algorithms were based on a finite, but
prohibitively large, abstraction (the region graph or the full backward stable
graph). Our algorithm uses XSB-style tabling with constraints. Our methodology
is more general than those followed in the previous approaches in the sense
that our algorithm can be used to decide whether two timed systems are
\emph{alternating timed bisimilar}.
Springer
2001
Conference-Paper
http://edoc.mpg.de/519772
Ramakrishnan, I.V.: Proceedings of the 3rd International Symposium on Practical Aspects of Declarative Languages, Springer, 245-258 (2001)
en
oai:edoc.mpg.de:5197732010-12-0287:932
On the complexity of inference about probabilistic relational models
Jaeger, Manfred
We investigate the complexity of probabilistic inference from
knowledge bases that encode probability distributions on finite domain
relational structures.
Our interest here lies in the
complexity in terms of the domain under consideration in a specific
application instance. We obtain the result that assuming NETIME$\neq$ETIME
this problem is not polynomial for reasonably expressive representation
systems. The main consequence of this result is that it is unlikely
to find inference techniques with a better
worst-case behavior than the commonly employed strategy of
constructing standard Bayesian networks over ground atoms
(knowledge based model construction).
2000
Article
http://edoc.mpg.de/519773
urn:ISSN:0004-3702
Artificial Intelligence, v.117, 297-308 (2000)
en
oai:edoc.mpg.de:5198122011-07-0887:932
A Uniform Constraint-based Framework for the Verification of Infinite State Systems
Mukhopadhyay, Supratik
Universität des Saarlandes
2001
PhD-Thesis
http://edoc.mpg.de/519812
en
oai:edoc.mpg.de:5198162010-12-0287:932
The lexicographic closure as a revision process
Booth, Richard
The connections between nonmonotonic reasoning and belief
revision are well-known. A central problem in the area of
nonmonotonic reasoning is the problem of default entailment, i.e.,
when should an item of default information representing "if A is
true then, normally, B is true" be said to follow from a given set of
items of such information. Many answers to this question have
been proposed but, surprisingly, virtually none have attempted
any explicit connection to belief revision. The aim of this paper is
to give an example of how such a connection can be made by
showing how the lexicographic closure of a set of defaults may be
conceptualised as a process of iterated revision by sets of
sentences. Specifically we use the revision process of Nayak.
?
2000
Conference-Paper
http://edoc.mpg.de/519816
Baral, C.; Truszczynski, M.: Proceedings of the 8th International Workshop on Non-Monotonic Reasoning (NMR 2000), ? (2000)
en
oai:edoc.mpg.de:5198172010-12-0287:932
Constraints as Data: a New Perspective on Inferring Probabilities
Jaeger, Manfred
We present a new approach to inferring a probability distribution
which is incompletely specified by a number of linear constraints.
We argue that the currently most popular approach of entropy
maximization depends on a ``constraints as knowledge'' interpretation
of the constraints, and that a different ``constraints as data''
perspective leads to a completely different type of inference
procedures by statistical methods. With statistical methods
some of the counterintuitive results of entropy maximization
can be avoided, and inconsistent sets of constraints can be
handled just like consistent ones. A particular statistical
inference method is developed and shown to have a
nice robustness property.
Morgan Kaufmann
2001
Conference-Paper
http://edoc.mpg.de/519817
urn:ISBN:1-55860-777-3
Nebel, Bernhard: Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI-01), Morgan Kaufmann, 755-760 (2001)
en
oai:edoc.mpg.de:5198182010-12-0287:932
Complex Probabilistic Modeling with Recursive Relational Bayesian Networks
Jaeger, Manfred
A number of representation systems have been proposed that
extend the purely propositional Bayesian network paradigm
with representation tools for some types of first-order
probabilistic dependencies. Examples of such systems are
dynamic Bayesian networks and systems for knowledge based
model construction. We can identify the representation of
probabilistic relational
models as a common well-defined semantic
core of such systems.
Recursive relational Bayesian networks (RRBNs) are a
framework for the representation of probabilistic relational models.
A main design goal for RRBNs
is to achieve greatest possible expressiveness
with as few elementary syntactic constructs as possible. The advantage
of such an approach is that a system based on a small number
of elementary constructs will be much more amenable to a thorough
mathematical investigation of its semantic and algorithmic
properties than a system based on a larger number of high-level
constructs. In this paper we show that with RRBNs
we have achieved our goal, by showing, first,
how to solve within that framework a number of non-trivial
representation problems. In the second part of the paper
we show how to construct from a RRBN and a specific query,
a standard Bayesian network in which the answer to the query
can be computed with standard inference algorithms. Here the
simplicity of the underlying representation framework
greatly facilitates the development of simple algorithms
and correctness proofs. As a result we obtain a construction
algorithm that even for RRBNs that represent models for complex first-order
and statistical dependencies generates standard Bayesian networks
of size polynomial in the size of the domain given in a specific
application instance.
2001
Article
http://edoc.mpg.de/519818
urn:ISSN:1012-2443
Annals of Mathematics and Artificial Intelligence, v.32, 179-220 (2001)
en
oai:edoc.mpg.de:5198192010-12-0287:932
Automatic Derivation of Probabilistic Inference Rules
Jaeger, Manfred
A probabilistic inference rule is a general rule that
provides bounds on a target probability given constraints on
a number of input probabilities. Example: from
$P(A | B) \leq r$\ infer $P(\neg A | B) \in [1-r,1]$. Rules of
this kind have been studied extensively as a deduction
method for propositional probabilistic logics. Many different
rules have been proposed, and their validity proved --
often with substantial effort. Building on previous work
by T. Hailperin, in this paper we show that probabilistic
inference rules can be derived automatically, i.e. given
the input constraints and the target probability, one
can automatically derive the optimal bounds on the target
probability as a functional expression in the parameters
of the input constraints.
2001
Article
http://edoc.mpg.de/519819
urn:ISSN:0888-613X
International Journal of Approximate Reasoning, v.28, 1-22 (2001)
en
oai:edoc.mpg.de:5198302010-12-0287:932
A new meta-complexity theorem for bottom-up logic programs
Ganzinger, Harald
McAllester, David
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/519830
urn:ISBN:3-540-42254-4
Goré, Rajeev; Leitsch, Alexander; Nipkow, Tobias: Automated reasoning : First International Joint Conference, IJCAR 2001, Springer, 514-528 (2001)
en
oai:edoc.mpg.de:5198312010-12-0287:932
Context trees
Ganzinger, Harald
Nieuwenhuis, Robert
Nivela, Pilar
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/519831
urn:ISBN:3-540-42254-4
Goré, Rajeev; Leitsch, Alexander; Nipkow, Tobias: Automated reasoning : First International Joint Conference, IJCAR 2001, Springer, 242-256 (2001)
en
oai:edoc.mpg.de:5198322010-12-0287:932
Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems
Ganzinger, Harald
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/519832
urn:ISBN:0-7695-1281-x
Williams, Denise A.: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS-01), IEEE, 81-90 (2001)
en
oai:edoc.mpg.de:5198332010-12-0287:932
Constraints and Theorem Proving
Ganzinger, Harald
Nieuwenhuis, Robert
This paper is a tutorial on methods
for first-order theorem proving with constraints.
Springer
2001
Conference-Paper
http://edoc.mpg.de/519833
urn:ISBN:3-540-41950-0
Comon, Hubert; Marché, Claude; Treinen, Ralf: Contraints in Computational Logics, International Summer School (CCL-99), Springer, 159-201 (2001)
en
oai:edoc.mpg.de:5198342010-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/519834
Journal of the ACM, v.48, 70-109 (2001)
en
oai:edoc.mpg.de:5198382011-07-0887:932
Ein Frontend für die Anwendung von Model Checking auf die Analyse von Array Bounds für C Programme
Jung, Georg
Universität des Saarlandes
2001
Thesis
http://edoc.mpg.de/519838
de
oai:edoc.mpg.de:5198402011-07-0787:932
Einige Optimierungsmethoden hierarchischer Schaltkreise
Gamkrelidze, Alexander
Universität des Saarlandes
2001
PhD-Thesis
http://edoc.mpg.de/519840
de
oai:edoc.mpg.de:5198602010-12-0287:932
The Next WALDMEISTER Loop (Extended Abstract)
Hillenbrand, Thomas
Löchner, Bernd
Max-Planck-Institut für Informatik
2001
Conference-Paper
http://edoc.mpg.de/519860
de Nivelle, Hans; Schulz, Stephan: Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, Max-Planck-Institut für Informatik, 13-21 (2001)
en
oai:edoc.mpg.de:5198642010-12-0287:932
On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results
Sofronie-Stokkermans, Viorica
In this paper we give a method for automated theorem proving in the universal
theory of certain varieties of distributive lattices with well-behaved
operators. For this purpose, we use extensions of Priestley's representation
theorem for distributive lattices. We first establish a link between
satisfiability of universal sentences with respect to varieties of distributive
lattices with operators and satisfiability with respect to certain classes of
relational structures. We then use these results for giving a method for
translation to clause form of universal sentences in such varieties, and obtain
decidability and complexity results for the universal theory of some such
varieties. The advantage is that we avoid the explicit use of the full
algebraic structure of such lattices, instead using sets endowed with a
reflexive and transitive relation and with additional functions and relations.
We first studied this type of relationships in the context of finitely-valued
logics and then extended the ideas to more
general non-classical logics. This paper shows that the idea is much more
general. In particular, the method presented here subsumes both existing
methods for translating modal logics to classical logic and methods for
automated theorem proving in finitely-valued logics based on distributive
lattices with operators.
Springer
Copyright Springer
1999
Conference-Paper
http://edoc.mpg.de/519864
Ganzinger, Harald: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), Springer, 157-171 (1999)
en
oai:edoc.mpg.de:5198722010-12-0287:932
Modeling Interaction by Sheaves and Geometric Logic
Sofronie-Stokkermans, Viorica
Stokkermans, Karel
In this paper we show that, given a family of interacting systems, many notions
which are important for expressing properties of systems can be modeled as
sheaves over a suitable topological space.
In such contexts, geometric logic can be used to test whether ``local''
properties can be lifted to a global level.
We develop a way to use this method in the study of interacting systems,
illustrated by examples.
Springer
Copyright Springer
1999
Conference-Paper
http://edoc.mpg.de/519872
urn:ISBN:3-540-66412-2
Ciobanu, Gabriel; Paun, Gheorghe: Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), Springer, 512-523 (1999)
en
oai:edoc.mpg.de:5198742010-12-0287:932
Resolution-based theorem proving for SHn-logics
Sofronie-Stokkermans, Viorica
In this paper we illustrate by means of an example, namely $SHn$-logics,
a method for translation to clause form and automated theorem proving for
first-order many-valued logics based on distributive lattices with operators.
Springer
Copyright Springer
2000
Conference-Paper
http://edoc.mpg.de/519874
urn:ISBN:3-540-67190-0
Automated Deduction in Classical and Non-Classical Logic (Selected Papers of FTP'98), Springer, 268-282 (2000)
en
oai:edoc.mpg.de:5198782010-12-0287:932
On unification for bounded distributive lattices
Sofronie-Stokkermans, Viorica
We give a resolution-based procedure for deciding unifiability
in the variety of bounded distributive lattices. The main idea
is to use a structure-preserving translation to clause form to
reduce the problem of testing the satisfiability of a unification
problem ${\cal S}$ to the problem of checking the satisfiability
of a set $\Phi_{\cal S}$ of (constrained) clauses. These ideas
can be used for unification with free constants and for
unification with linear constant restrictions. Complexity issues
are also addressed.
Springer
Copyright Springer Verlag
2000
Conference-Paper
http://edoc.mpg.de/519878
urn:ISBN:3-540-67664-3
McAllester, David: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), Springer, 465-481 (2000)
en
oai:edoc.mpg.de:5198882010-12-0287:932
First-Order Atom Definitions Extended
Afshordel, Bijan
Hillenbrand, Thomas
Weidenbach, Christoph
Springer
2001
Conference-Paper
http://edoc.mpg.de/519888
Nieuwenhuis, Robert; Voronkov, Andrei: Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), Springer, 309-319 (2001)
en
oai:edoc.mpg.de:5198952010-12-0287:932
On the Evaluation of Indexing Techniques for Theorem Proving
Nieuwenhuis, Robert
Hillenbrand, Thomas
Riazanov, Alexandre
Voronkov, Andrei
Springer
2001
Conference-Paper
http://edoc.mpg.de/519895
urn:ISBN:3-540-42254-5
Goré, Rajeev; Leitsch, Alexander; Nipkow, Tobias: Automated reasoning : First International Joint Conference, IJCAR 2001, Springer, 257-271 (2001)
en
oai:edoc.mpg.de:5199052010-12-0287:932
Chaining Techniques for Automated Theorem Proving in Many-Valued Logics
Ganzinger, Harald
Sofronie-Stokkermans, Viorica
We apply chaining techniques to automated theorem proving in many-valued
logics. In particular, we show that superposition specializes to a refined
version of the many-valued resolution rules introduced by Baaz and Fermüller,
and that ordered chaining can be specialized to a refutationally complete
inference system for regular clauses.
IEEE
2000
Conference-Paper
http://edoc.mpg.de/519905
urn:ISBN:0-7695-0692-5
Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL-00), IEEE, 337-344 (2000)
en