2020-10-30T11:26:09Zhttp://edoc.mpg.de/ac_ft_oai.ploai:edoc.mpg.de:2018102010-12-0287:932
Conference-Paper
Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER
English
Elsevier
Amsterdam, The Netherlands
2003
2004-06-22
1
13
Valencia, Spain
2003-06-12
Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03
Electronic Notes in Theoretical Computer Science
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=9134&did=201810&ver=0
T.
Hillenbrand
Thomas
I.
Dahn
Ingo
L.
Vigneron
Laurent
C1256104005ECAFC-13192155732F5DD1C1256D32004620FA-Hillenbrand2003
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2018232010-12-0287:932
Conference-Paper
The New WALDMEISTER Loop at Work
English
Springer
Berlin, Germany
2003
2004-06-23
317
321
Miami, Florida
2003-07-28
Automated deduction, CADE-19 : 19th International Conference on Automated Deduction
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=9137&did=201823&ver=0
J.-M.
Gaillourdet
Jean-Marie
T.
Hillenbrand
Thomas
B.
Löchner
Bernd
H.
Spies
Hendrik
F.
Baader
Franz
C1256104005ECAFC-F7AE319E928299C3C1256D01002DD440-GaillourdetHillenbrandLoechner2003
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2018532010-12-0287:932
Conference-Paper
Superposition modulo a Shostak Theory
English
Springer
Berlin, Germany
2003
2004-06-17
182
196
Miami, Florida
2003-07-28
Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=9147&did=201853&ver=0
H.
Ganzinger
Harald
T.
Hillenbrand
Thomas
U.
Waldmann
Uwe
F.
Baader
Franz
3-540-40559-3
C1256104005ECAFC-4489C55BD13D7669C1256CFE005A7257-GanzingerHillenbrandWaldmann2003
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2018942010-12-0287:932
Article
On Using Ground Joinable Equations in Equational Theorem Proving
English
2003
2004-06-23
217
233
Journal of Symbolic Computation
36
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.
No
expertsonly
published
joureview
http://edoc.mpg.de/get.epl?fid=9153&did=201894&ver=0
J.
Avenhaus
Jürgen
T.
Hillenbrand
Thomas
B.
Löchner
Bernd
0747-7171
C1256104005ECAFC-A129A5E170AD94F0C1256D01002C84B9-AvenhausHillenbrandLoechner2003
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2018982010-12-0287:932
PhD-Thesis
A Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning
English
Universität des Saarlandes
Saarbrücken, Saarland
2003
2004-06-29
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.
notspecified
http://edoc.mpg.de/get.epl?fid=9155&did=201898&ver=0
P.
Maier
Patrick
C1256104005ECAFC-97A2749806AF9DF1C1256EC2005EAF70-Maier2003
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2020192010-12-0287:932
Conference-Paper
New Directions in Instantiation-Based Theorem Proving
English
IEEE
Los Alamitos, USA
2003
2004-06-17
55
64
Ottawa, Canada
2003-06-22
18th Annual IEEE Symposium on Logic in Computer Science (LICS-03)
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=9176&did=202019&ver=0
H.
Ganzinger
Harald
K.
Korovin
Konstantin
P.
Kolaitis
Phokion
0-7695-1884-2
C1256104005ECAFC-9F899010FD50E7D7C1256D170066FF4B-GanzingerKorovin-03-lics
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2020262010-12-0287:932
Conference-Paper
A Representation Theorem and Applications
English
Springer
Berlin, Germany
2003
2004-06-17
50
61
Aalborg, Denmark
2003-07-02
Symbolic and Quantitative Approaches to Reasoning with Uncertainty :
7th European Conference, ECSQARU 2003
Lecture Notes in Computer Science
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=9177&did=202026&ver=0
M.
Jaeger
Manfred
T.D.
Nielsen
Thomas D.
N.L.
Zhang
Nevin L.
3-540-40494-5
C1256104005ECAFC-8F468E8BDA25A19FC1256D01002C63A8-JaegerECSQARU03
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2020272010-12-0287:932
Conference-Paper
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
English
Springer
Berlin, Germany
2003
2004-06-17
335
349
Miami, Florida
2003-07-28
Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=9178&did=202027&ver=0
H.
Ganzinger
Harald
J.
Stuber
Jürgen
F.
Baader
Franz
3-540-40559-3
C1256104005ECAFC-834A2D263C7BFE3F00256D200035E7D7-GanzingerStuber-2003-cade
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2020322010-12-0287:932
Conference-Paper
Subsumption of Concepts in FL_0 for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACE-complete
English
CEUR
Aachen, Germany
2003
2004-06-22
56
64
Rome, Italy
2003-09-05
2003 International Workshop on Description Logics (DL-03)
CEUR Workshop Proceedings
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=9179&did=202032&ver=0
Y.
Kazakov
Yevgeny
H.
de Nivelle
Hans
D.
Calvanese
Diego
G.
De Giacomo
Giuseppe
E.
Franconi
Enrico
1613-0073
C1256104005ECAFC-746B1C632282C1C9C1256E23006ADC00-Kazakov03SubsumptionFLzero
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2312522010-12-0287:932
Article
Fast Term Indexing with Coded Context Trees
English
2004
2005-02-02
103
120
Journal of Automated Reasoning
32
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.
No
expertsonly
published
joureview
http://edoc.mpg.de/get.epl?fid=13336&did=231252&ver=0
H.
Ganzinger
Harald
R.
Nieuwenhuis
Robert
P.
Nivela
Pilar
C1256104005ECAFC-B0EF8A197F4BBBE400256D20003B728C-GanzingerNieuwenhuisNivela-03-jar
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2312582010-12-0287:932
Conference-Paper
A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment
English
Springer
Berlin, Germany
2004
2005-02-02
372
384
Lisbon, Portugal
2004-09-27
Logics in artificial intelligence : 9th European Conference, JELIA 2004
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=13337&did=231258&ver=0
Y.
Kazakov
Yevgeny
J.J.
Alferes
José Júlio
J.
Leite
João
3-540-23242-7
C1256104005ECAFC-3E0C7DF49217CA81C1256EE20080EDAC-Kazakov04GF2N
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
© Springer-Verlag
oai:edoc.mpg.de:2312652010-12-0287:932
Conference-Paper
Robust Pole Clustering of Parametric Uncertain Systems Using Interval Methods
English
Publ. for the International Federation of Automatic Control by Elsevier
Oxford
2004
2005-02-03
323
328
Milano
2003-07-07
Robust control design 2003 : (ROCOND 2003) ; a proceedings volume from the 4th IFAC symposium
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=13338&did=231265&ver=0
S.
Ratschan
Stefan
J.
Vehi
Josep
S.
Bittanti
Sergio
0-08-044012-6
C1256104005ECAFC-13B500BDBD6D466DC1256D0200300F64-Ratschan2002
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2312712010-12-0287:932
Conference-Paper
A Superposition View on Nelson-Oppen
English
CEUR
Aachen
2004
2005-02-02
16
20
Cork, Ireland
2004-08-04
Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning
CEUR Workshop Proceedings
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=13339&did=231271&ver=0
T.
Hillenbrand
Thomas
U.
Sattler
Ulrike
1613-0073
C1256104005ECAFC-8EAD4DC962EDE15BC1256EE40054344A-Hillenbrand2004
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2312722010-12-0287:932
Thesis
Instance Generation Methods for Automated Reasoning
English
Universität des Saarlandes
Saarbrücken, Saarland
2005-04-27
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=13340&did=231272&ver=0
S.
Jacobs
Swen
C1256104005ECAFC-288285D9C047581FC1256FC0004BA71E-Jacobs2004
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2319652010-12-0287:932
Conference-Paper
Robust Pole Clustering of Parametric Uncertain Systems Using Interval Methods
English
Publ. for the International Federation of Automatic Control by Elsevier
Oxford
2004
2005-02-03
323
328
Milano
2003-07-07
Robust control design 2003 : (ROCOND 2003) ; a proceedings volume from the 4th IFAC symposium
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=13504&did=231965&ver=0
S.
Ratschan
Stefan
J.
Vehi
Josep
S.
Bittanti
Sergio
0-08-044012-6
C1256104005ECAFC-13B500BDBD6D466DC1256D0200300F64-Ratschan2002
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2319972010-12-0287:932
Conference-Paper
A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment
English
Springer
Berlin, Germany
2004
2005-02-02
372
384
Lisbon, Portugal
2004-09-27
Logics in artificial intelligence : 9th European Conference, JELIA 2004
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=13511&did=231997&ver=0
Y.
Kazakov
Yevgeny
J.J.
Alferes
José Júlio
J.
Leite
João
3-540-23242-7
C1256104005ECAFC-3E0C7DF49217CA81C1256EE20080EDAC-Kazakov04GF2N
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
© Springer-Verlag
oai:edoc.mpg.de:2320022010-12-0287:932
Conference-Paper
A Superposition View on Nelson-Oppen
English
CEUR
Aachen
2004
2005-02-02
16
20
Cork, Ireland
2004-08-04
Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning
CEUR Workshop Proceedings
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=13514&did=232002&ver=0
T.
Hillenbrand
Thomas
U.
Sattler
Ulrike
1613-0073
C1256104005ECAFC-8EAD4DC962EDE15BC1256EE40054344A-Hillenbrand2004
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2320322010-12-0287:932
Thesis
Instance Generation Methods for Automated Reasoning
English
Universität des Saarlandes
Saarbrücken, Saarland
2004
2005-04-27
diplom
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=13522&did=232032&ver=0
S.
Jacobs
Swen
C1256104005ECAFC-288285D9C047581FC1256FC0004BA71E-Jacobs2004
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2320342010-12-0287:932
Article
Fast Term Indexing with Coded Context Trees
English
2004
2005-02-02
103
120
Journal of Automated Reasoning
32
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.
No
expertsonly
published
joureview
http://edoc.mpg.de/get.epl?fid=13524&did=232034&ver=0
H.
Ganzinger
Harald
R.
Nieuwenhuis
Robert
P.
Nivela
Pilar
C1256104005ECAFC-B0EF8A197F4BBBE400256D20003B728C-GanzingerNieuwenhuisNivela-03-jar
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2378662010-12-0287:932
Report
Summaries for while programs with recursion
English
Max-Planck-Institut für Informatik
Saarbrücken
2004-12
2004-2-007
Max-Planck-Institut für Informatik <Saarbrücken>: Research Report
Max-Planck-Institut für Informatik <Saarbrücken>
expertsonly
18 p.
http://edoc.mpg.de/get.epl?fid=14940&did=237866&ver=0
S.
Wagner
Silke
MPI-I-2004-2-007
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2378702010-12-0287:932
Report
Intuitionistic LTL and a New Characterization of Safety and Liveness
English
Max-Planck-Institut für Informatik
Saarbrücken
2004-08
2004-2-002
Max-Planck-Institut für Informatik <Saarbrücken>: Research Report
Max-Planck-Institut für Informatik <Saarbrücken>
expertsonly
18 p.
http://edoc.mpg.de/get.epl?fid=14941&did=237870&ver=0
P.
Maier
Patrick
MPI-I-2004-2-002
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2378712010-12-0287:932
Report
Resolution decision procedures for the guarded fragment with transitive guards
English
Max-Planck-Institut für Informatik
Saarbrücken
2004-04
2004-2-001
Max-Planck-Institut für Informatik <Saarbrücken>: Research Report
Max-Planck-Institut für Informatik <Saarbrücken>
expertsonly
25 p.
http://edoc.mpg.de/get.epl?fid=14943&did=237871&ver=0
H.
de Nivelle
Hans
Y.
Kazakov
Yevgeny
MPI-I-2004-2-001
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2790752010-12-0287:932
Conference-Paper
An Abstract Model of Routing in Mobile Ad Hoc Networks
English
DAIMI
Aarhus, Denmark
2005
2006-06-19
137
156
Aarhus, Denmark
2005-10-24
Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=22477&did=279075&ver=0
C.
Yuan
Cong
J.
Billington
Jonathan
J.
Freiheit
Jörn
C1256104005ECAFC-4F554DB9FD935C32C12570A8004C674E-Freiheit2005a
MPI für Informatik
Programming Logics Group
2006
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2790882011-05-0587:932
Conference-Paper
Enhanced Workflow Models as a Tool for Judicial Practitioners
English
Springer
Berlin, Germany
2005
2006-06-09
26
27
Agia Napa, Cyprus
2005-10-31
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
Lecture Notes in Computer Science
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.
No
expertsonly
published
notspecified
http://edoc.mpg.de/get.epl?fid=22478&did=279088&ver=0
J.
Freiheit
Jörn
S.
Münch
Susanne
H.
Schöttle
Hendrik
G.
Sijanski
Grozdana
F.
Zangl
Fabrice
R.
Meersman
Robert
Z.
Tari
Zahir
P.
Herrero
Pilar
G.
Méndez
Gonzalo
L.
Cavedon
Lawrence
D.
Martin
David
A.
Hinze
Annika
G.
Buchanan
George
M. S.
Pérez
María S.
V.
Robles
Víctor
J.
Humble
Jan
A.
Albani
Antonia
J. L.
Dietz
Jan L.G.
H.
Panetto
Herve
M.
Scannapieco
Monica
T.
Halpin
Terry
P.
Spyns
Peter
J. M.
Zaha
Johannes Maria
E.
Zimány
Esteban
E.
Stefanakis
Emmanuel
T.
Dillon
Tharam
L.
Feng
Ling
M.
Jarrar
Mustafa
J.
Lehmann
Jos
A.
de Moor
Aldo
E.
Duval
Erik
L.
Aroyo
Lora
3-540-29739-1
C1256104005ECAFC-9534E1575B414174C12570B20035B569-Freiheit2005b
MPI für Informatik
Programming Logics Group
2006
2011-05-05 10:31:39.945442
oai:edoc.mpg.de:2791012010-12-0287:932
Conference-Paper
Integration of a Software Model Checker into Isabelle
English
Springer
Berlin, Germany
2005
2006-01-17
381
395
Montego Bay, Jamaica
2005-12-02
Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=22479&did=279101&ver=0
M.
Daum
Matthias
S.
Maus
Stefan
N.
Schirmer
Norbert
M.N.
Seghir
Mohammed Nassim
G.
Sutcliffe
Geoff
A.
Voronkov
Andrei
3-540-30553-X
C1256104005ECAFC-AC084AE06EB1D6B2C12570D700608013-DMSSISAMC2005
MPI für Informatik
Programming Logics Group
2006
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:2791212010-12-0287:932
Conference-Paper
Comparing Instance Generation Methods for Automated Reasoning
English
Springer
Berlin, Germany
2005
2005-12-21
153
168
Koblenz, Germany
2005-09-14
Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX 2005
Lecture Notes in Computer Science
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=22481&did=279121&ver=0
S.
Jacobs
Swen
U.
Waldmann
Uwe
B.
Beckert
Bernhard
3-540-28931-3
C1256104005ECAFC-B54B67CC129A5649C1257085003336D5-JacobsWaldmann2005
MPI für Informatik
Programming Logics Group
2006
2010-12-02 11:37:35.381871
Copyright 2005 Springer-Verlag
oai:edoc.mpg.de:3144872010-12-0287:932
Conference-Paper
Field Constraint Analysis
English
Springer
Berlin, Germany
2006
2007-02-16
157
173
Charleston, SC, USA
2006-01-08
Verification, Model Checking, and Abstract Interpretation : 7th International Conference, VMCAI 2006
Lecture Notes in Computer Science
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=35787&did=314487&ver=0
T.
Wies
Thomas
V.
Kuncak
Viktor
P.
Lam
Patrick
A.
Podelski
Andreas
M.C.
Rinard
Martin C.
E.A.
Emerson
E. Allen
K.S.
Namjoshi
Kedar S.
C1256104005ECAFC-761CADE4F91377D6C12570B000587F60-WiesETAL06FieldConstraintAnalysis
MPI für Informatik
Programming Logics Group
2007
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:3145652011-07-0887:932
PhD-Thesis
Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment
English
Universität des Saarlandes
Saarbrücken, Saarland
2006-03-17
2007-04-10
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=35825&did=314565&ver=0
Y.
Kazakov
Yevgeny
C1256104005ECAFC-C84B4763BC1994CDC1257145004631F6-Kazakov2005
MPI für Informatik
Programming Logics Group
2011-07-08 12:57:08.435315
oai:edoc.mpg.de:3146012010-12-0287:932
Thesis
Abstrakte Übergangsrelationen als Mittel zur Verifikation von Programmeigenschaften
German
Universität des Saarlandes
Saarbrücken, Saarland
2006-11-29
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
expertsonly
http://edoc.mpg.de/get.epl?fid=35840&did=314601&ver=0
M.
Schäf
Martin
C1256104005ECAFC-9A16D39FBB0ADE2EC12571450044FF2C-Schaef2005
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:3566252010-12-0287:932
Conference-Paper
Precise Thread-Modular Verification
English
Springer
Berlin, Germany
2007
2008-03-07
218
232
Kongens Lyngby, Denmark
2007-05-08
2007-05-08
Static Analysis : 14th International Symposium, SAS 2007
Filé, Gilberto; Riis Nielson, Hanne
Lecture Notes in Computer Science
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=45068&did=356625&ver=0
A.
Malkis
Alexander
A.
Podelski
Andreas
A.
Rybalchenko
Andrey
3-540-74060-0
10.1007/978-3-540-74061-2_14
C12573CC004A8E26-7E5E80A3B2C2F34BC12572D500339DAC-MalkisPodelskiRybalchenkoSAS2007
MPI für Informatik
Programming Logics Group
2008
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:3566262010-12-0287:932
Conference-Paper
Region Stability Proofs for Hybrid Systems
English
Springer
Berlin, Germany
2007
2008-03-07
320
335
Salzburg, Austria
2007-10-03
2007-10-05
Formal Modeling and Analysis of Timed Systems : 5th International Conference, FORMATS 2007
Raskin, J.-F.; Thiagarajan, P.S.
Lecture Notes in Computer Science
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=45069&did=356626&ver=0
A.
Podelski
Andreas
S.
Wagner
Silke
3-540-75453-9
10.1007/978-3-540-75454-1_23
C12573CC004A8E26-226A10E7924A08F0C12573160032D6C1-PodelskiWagner03_2007
MPI für Informatik
Programming Logics Group
2008
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:3566282010-12-0287:932
Conference-Paper
Theory Instantiation
English
Springer
Berlin, Germany
2006
2008-03-07
497
511
Phnom Penh, Cambodia
2006-11-13
2006-11-17
Logic for Programming, Artificial Intelligence, and Reasoning : 13th International Conference, LPAR 2006
Hermann, Miki; Voronkov, Andrei
Lecture Notes in Artificial Intelligence
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=45070&did=356628&ver=0
H.
Ganzinger
Harald
K.
Korovin
Konstantin
3-540-48281-4
10.1007/11916277_34
C12573CC004A8E26-1CBDABE9C16AAE05C12573FA002F08C9-GK2007
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:3566292010-12-0287:932
Conference-Paper
Path Invariants
English
ACM
New York, NY, USA
2007
2008-03-07
300
309
San Diego, CA, USA
2007-06-10
2007-06-13
PLDI'07 : Proceedings of the 2007 Conference on Programming Language Design and Implementation
Ferrante, Jeanne; McKinley, Kathryn S.
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=45071&did=356629&ver=0
D.
Beyer
Dirk
T.
Henzinger
Thomas
R.
Majumdar
Rupak
A.
Rybalchenko
Andrey
978-1-59593-633-2
10.1145/1250734.1250769
C12573CC004A8E26-48258C5145573B41C12572A2007E9680-Rybalchenko2007PLDI-Paths
MPI für Informatik
Programming Logics Group
2008
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:3566402010-12-0287:932
Conference-Paper
Proving Thread Termination
English
ACM
New York, NY, USA
2007
2008-03-07
320
330
San Diego, CA, USA
2007-06-10
2007-06-13
PLDI'07 : Proceedings of the 2007 Conference on Programming Language Design and Implementation
Ferrante, Jeanne; McKinley, Kathryn S.
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=45082&did=356640&ver=0
B.
Cook
Byron
A.
Podelski
Andreas
A.
Rybalchenko
Andrey
978-1-59593-633-2
10.1145/1250734.1250771
C12573CC004A8E26-0E3286174490BE72C12572A2007E5F0F-Rybalchenko2007PLDI-Threads
MPI für Informatik
Programming Logics Group
2008
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:3566772010-12-0287:932
Conference-Paper
Proving that programs eventually do something good
English
ACM
New York, USA
2007
2008-03-07
265
276
Nice, France
2007-03-18
2007-03-18
Conference Record of POPL® 2007 : The 34th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages
Hofmann, Martin; Felleisen, Matthias
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=45095&did=356677&ver=0
B.
Cook
Byron
A.
Gotsman
Alexey
A.
Podelski
Andreas
A.
Rybalchenko
Andrey
M.
Vardi
Moshe
1-59593-575-4
10.1145/1190216.1190257
C12573CC004A8E26-F0CC8AA9A7B40F8AC12572A2007E1277-Rybalchenko2007POPL
MPI für Informatik
Programming Logics Group
2008
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:3566782012-01-1087:932
Report
A Method and a Tool for Automatic Verification of Region Stability for Hybrid Systems
English
Max-Planck-Institut für Informatik
Saarbrücken
2007
2008-03-07
MPI-I-2007-2-001
Max-Planck-Institut für Informatik / Research Report
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.
No
expertsonly
46 p.
http://edoc.mpg.de/get.epl?fid=45096&did=356678&ver=0
A.
Podelski
Andreas
S.
Wagner
Silke
C12573CC004A8E26-5EFB11340F0182DBC12572970053D04E-PodelskiWagner01_2007
MPI-I-2007-2-001
MPI für Informatik
Programming Logics Group
2008
2012-01-10 13:03:25.217655
oai:edoc.mpg.de:3567072010-12-0287:932
Conference-Paper
ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement
English
Springer
Berlin, Germany
2007
2008-03-07
245
259
Nice, France
2007-01-14
2007-01-15
Practical aspects of declarative languages : 9th International Symposium, PADL 2007
Hanus, Michael
Lecture Notes in Computer Science
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=45111&did=356707&ver=0
A.
Podelski
Andreas
A.
Rybalchenko
Andrey
3-540-69608-3
10.1007/978-3-540-69611-7_16
C12573CC004A8E26-B25DA1215596A4A6C12572A2007D7B25-Rybalchenko2007PADL
MPI für Informatik
Programming Logics Group
2008
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:3567082010-12-0287:932
Conference-Paper
Invariant Synthesis for Combined Theories
English
Springer
Berlin, Germany
2007
2008-03-07
378
394
Nice, France
2007-01-14
2007-01-16
Verification, Model Checking, and Abstract Interpretation : 8th International Conference, VMCAI 2007
Cook, Byron; Podelski, Andreas
Lecture Notes in Computer Science
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=45112&did=356708&ver=0
D.
Beyer
Dirk
T.
Henzinger
Thomas
R.
Majumdar
Rupak
A.
Rybalchenko
Andrey
978-3-540-69735-0
10.1007/978-3-540-69738-1_27
C12573CC004A8E26-C4C46977FD7517A0C12572A2007CFDE3-Rybalchenko2007VMCAI-InvGen
MPI für Informatik
Programming Logics Group
2008
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5194552011-07-0487:932
Thesis
A Reinterpretation of the Deductive Tableaux System in Higher-Order Logic
English
Universität des Saarlandes
Saarbrücken, Saarland
1995
2010-03-12
master
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=72770&did=519455&ver=0
A.
Ayari
Abdelwaheb
C1256104005ECAFC-0524ABFC630F5348C12562F8005E190D-Abdu95
MPI für Informatik
Programming Logics Group
2011-07-04 11:28:56.226387
oai:edoc.mpg.de:5195062010-12-0287:932
Conference-Paper
Relational Bayesian Networks
English
Morgan Kaufmann
San Francisco, USA
1997
2010-03-12
266
273
Providence, USA
1997
Proceedings of the 13th Conference of Uncertainty in Artificial Intelligence (UAI-13)
Geiger, Dan; Shenoy, Prakash Pundalik
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72771&did=519506&ver=0
M.
Jaeger
Manfred
1-55860-485-5
C1256104005ECAFC-41A7C85CEC93AC25C12564810014BF45-Jaeger97UAI
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5195302011-07-0887:932
Thesis
Transformations of First-Order Formulae for Automated Reasoning
English
Universität des Saarlandes
Saarbrücken, Saarland
1995-07-28
2010-03-12
master
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=72772&did=519530&ver=0
G.
Rock
Georg
C1256104005ECAFC-64249D80170816ACC12562F8005EB17F-Rock95
MPI für Informatik
Programming Logics Group
2011-07-08 13:27:15.998041
oai:edoc.mpg.de:5195622011-07-0487:932
Thesis
A Calculus of Simplification for Superposition
English
Universität des Saarlandes
Saarbrücken, Saarland
1997
2010-03-12
master
expertsonly
http://edoc.mpg.de/get.epl?fid=72773&did=519562&ver=0
M.
Christen
Michael
C1256104005ECAFC-8DB9717BA22CB258C125659A0046C861-Christen97
MPI für Informatik
Programming Logics Group
2011-07-04 11:16:42.429479
oai:edoc.mpg.de:5195722011-07-0487:932
Thesis
Quantifier Elimination in Second-Order Predicate Logic
English
Universität des Saarlandes
Saarbrücken, Saarland
1996
2010-03-12
master
expertsonly
http://edoc.mpg.de/get.epl?fid=72774&did=519572&ver=0
T.
Engel
Thorsten
C1256104005ECAFC-96219E83E1111E5AC125647C0055F9D5-Engel96
MPI für Informatik
Programming Logics Group
2011-07-04 12:00:46.092857
oai:edoc.mpg.de:5195792011-07-0887:932
Thesis
Testing the Satisfiability of RPO Constraints
English
Universität des Saarlandes
Saarbrücken, Saarland
1997
2010-03-12
master
expertsonly
http://edoc.mpg.de/get.epl?fid=72775&did=519579&ver=0
J.-G.
Timm
Jan-Georg
C1256104005ECAFC-A31E480CFA2F5514C12565B70052EC7F-Timm97
MPI für Informatik
Programming Logics Group
2011-07-08 13:48:32.065791
oai:edoc.mpg.de:5196092011-07-0787:932
Thesis
Superposition Extended with Sorts
English
Universität Kaiserslautern
Saarbrücken, Saarland
1995
2010-03-12
master
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=72776&did=519609&ver=0
B.
Gaede
Bernd
C1256104005ECAFC-CA9CC4268DC03C99C12562F9005177DE-Gaede95-Mastersthesis
MPI für Informatik
Programming Logics Group
2011-07-07 15:31:16.621637
oai:edoc.mpg.de:5196102011-05-0687:932
Thesis
Parallel Unit Resulting Resolution
English
Universität des Saarlandes
Saarbrücken, Saarland
1996
2010-03-12
master
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=72777&did=519610&ver=0
C.
Meyer
Christoph
C1256104005ECAFC-CB093F8D8C5B3361C12562FA006018C0-Meyer-Diplom96
MPI für Informatik
Programming Logics Group
2011-05-06 11:56:36.729557
oai:edoc.mpg.de:5196122011-07-0487:932
Thesis
Static analysis of functional programs via Linear Logic
English
Universität des Saarlandes
Saarbrücken, Saarland
1996
2010-03-12
master
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=72778&did=519612&ver=0
A.
Bach
Alexander
C1256104005ECAFC-CC875A7179F97FCA412563EC007A42E9-Bach96
MPI für Informatik
Programming Logics Group
2011-07-04 11:29:57.596854
oai:edoc.mpg.de:5196242011-07-0487:932
Thesis
Effiziente Subsumption in Deduktionssystemen
German
Universität des Saarlandes
Saarbrücken, Saarland
1994
2010-03-12
master
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=72779&did=519624&ver=0
J.
Becker
Joachim
C1256104005ECAFC-E03D22F56DADD560412563EC0079F790-Becker94
MPI für Informatik
Programming Logics Group
2011-07-04 11:38:12.530049
oai:edoc.mpg.de:5196342010-12-0287:932
InBook
Resolution Theorem Proving
English
Elsevier
Amsterdam, the Netherlands
2001
2010-03-12
19
99
1
Handbook of Automated Reasoning
J. A. Robinson, A. Voronkov
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72780&did=519634&ver=0
L.
Bachmair
Leo
H.
Ganzinger
Harald
C1256104005ECAFC-E89AFB3982578341C125648E00502FAC-BachmairGanzinger-01-har
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
This chapter appeared in the Handbook of Automated Reasoning, North Holland,
2001.
oai:edoc.mpg.de:5196632010-12-0287:932
Conference-Paper
Measure Selection: Notions of Rationality and Representation Independence
English
Morgan Kaufmann
San Francisco, USA
1998
2010-03-12
274
281
Madison, USA
1998
Proceedings of the 14th Conference on Uncertainty in Artificial Intelligence (UAI-98)
Cooper, Gregory S.; Moral, Serafín
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72781&did=519663&ver=0
http://edoc.mpg.de/get.epl?fid=72782&did=519663&ver=0
M.
Jaeger
Manfred
C1256104005ECAFC-561F26CD4AE59824C12566F0005CDA28-Jaeger1998c
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5196642010-12-0287:932
Conference-Paper
Convergence Results for Relational Bayesian Networks
English
IEEE
Los Alamitos, USA
1998
2010-03-12
44
55
Indianapolis, USA
2003-07-08
2003-07-12
Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS-98)
Pratt, Vaughan
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72783&did=519664&ver=0
http://edoc.mpg.de/get.epl?fid=72784&did=519664&ver=0
M.
Jaeger
Manfred
C1256104005ECAFC-5EE56FAE8733BA9DC12566F0005C6F31-Jaeger1998b
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5196652010-12-0287:932
Conference-Paper
Reasoning About Infinite Random Structures with Relational Bayesian Networks
English
Morgan Kaufmann
San Francisco, USA
1998
2010-03-12
570
581
Trento, Italy
1998
Proceedings of the 6th International Conference on Principles of Knowledge Representation and Reasoning (KR-98)
Cohn, Anthony G.; Schubert, Lenhart; Shapiro, Stuart C.
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72785&did=519665&ver=0
http://edoc.mpg.de/get.epl?fid=72786&did=519665&ver=0
M.
Jaeger
Manfred
1-55860-554-1
C1256104005ECAFC-E176532FECBD651CC12566F0005BD749-Jaeger1998a
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5196742010-12-0287:932
Conference-Paper
$\forall\exists^\ast$-Equational Theory of Context Unification is $\Pi_1^0$-Hard
English
Springer
Berlin, Germany
1998
2010-03-12
597
606
Brno, Czech Republic
1998
Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS-98)
Brim, Lubos; Gruska, Jozef; Zlatuska, Jirí
Lecture Notes in Computer Science
\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}
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72787&did=519674&ver=0
S.
Vorobyov
Sergei
3-540-64827-5
C1256104005ECAFC-55E49321AE36A06D412566FA003E613F-Vorobyov1998MFCS
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5196752010-12-0287:932
Conference-Paper
Complexity of Nonrecursive Logic Programs with Complex Values
English
ACM
New York, USA
1998
2010-03-12
244
253
Saeattle, Washington, U.S.A.
Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS-98)
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72788&did=519675&ver=0
S.
Vorobyov
Sergei
A.
Voronkov
Andrei
0-89791-996-3
C1256104005ECAFC-64E8BC346A5A1603412566FA003D63DA-VorobyovVoronkov1998PODS
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5196772010-12-0287:932
Conference-Paper
Subtyping Functional+Nonempty Record Types
English
Springer
Berlin, Germany
1999
2010-03-12
285
297
Brno, Czech Republic
1999
Proceedings of the 12th International Workshop on Computer Science Logic (CSL-98), Annual Conference on the EACSL
Gottlob, Georg; Grandjean, Etienne; Seyr, Katrin
Lecture Notes in Computer Science
\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}
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72789&did=519677&ver=0
S.
Vorobyov
Sergei
3-540-65922-6
C1256104005ECAFC-B535BC26FE7E2720412566FA003F0BE5-Vorobyov1998CSL
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5196932010-12-0287:932
Conference-Paper
A Superposition Decision Procedure for the Guarded Fragment with Equality
English
IEEE
Los Alamitos, USA
1999
2010-03-12
295
303
Trento, Italy
2003-07-08
2003-07-12
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99)
Longo, Giuseppe
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72790&did=519693&ver=0
http://edoc.mpg.de/get.epl?fid=72791&did=519693&ver=0
H.
Ganzinger
Harald
H.
de Nivelle
Hans
0-7695-0158-3
C1256104005ECAFC-B613AAD4404037B3C1256744002BF554-GanzingerNivelle-99-lics
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5197292010-12-0287:932
InBook
A Resolution-Based Decision Procedure for Extensions of K4
English
CSLI
Stanford, USA
2001
2010-03-12
225
246
119
Advances in Modal Logic, Volume 2
Michael Zakharyaschev, Krister Segerberg, Maarten de Rijke, Heinrich Wansing
CSLI Lecture Notes
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72792&did=519729&ver=0
H.
Ganzinger
Harald
U.
Hustadt
Ullrich
C.
Meyer
Christoph
R.A.
Schmidt
Renate A.
1-57586-272-7
C1256104005ECAFC-0BECC945CC71EA19C125675A006045A2-Ganzinger-et-al-00-AIML
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5197482010-12-0287:932
Conference-Paper
Beyond Region Graphs: Symbolic Forward Analysis of Timed Automata
English
Springer
Berlin, Germany
1999
2010-03-12
232
244
Chennai, India
1999
Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS-99)
Ramanujam, R; Raman, V.
Lecture Notes in Computer Science
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72793&did=519748&ver=0
S.
Mukhopadhyay
Supratik
A.
Podelski
Andreas
3-540-66836-5
C1256104005ECAFC-CCD5912D3A4751474125682B0058EE57-MukhopadhyayPodelskiFSTTCS1999
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5197572010-12-0287:932
Conference-Paper
Fairness, Computable Fairness and Randomness
English
School of Computer Science, University of Birmingham
Birmingham
1999
2010-03-12
57
66
Eindhoven, the Netherlands
1999
Proceedings of the 2nd International Workshop on Probabilistic Methods in Verification (PROBMIV-99)
Kwiatkowska, Marta
Technical Report CSR-99-8
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72794&did=519757&ver=0
http://edoc.mpg.de/get.epl?fid=72795&did=519757&ver=0
M.
Jaeger
Manfred
C1256104005ECAFC-21ED7872A37ABC3FC125688F00626135-Jaeger99
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5197582011-07-0487:932
PhD-Thesis
Relations between Abstract Datatypes modeled as Abstract Datatypes
English
Universität des Saarlandes
Saarbrücken, Saarland
1999-05-21
2010-03-12
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=72796&did=519758&ver=0
H.
Baumeister
Hubert
C1256104005ECAFC-259AAD6E949570BFC12568A900543BDC-BaumeisterDiss99
MPI für Informatik
Programming Logics Group
2011-07-04 11:37:07.498296
oai:edoc.mpg.de:5197712011-07-0887:932
PhD-Thesis
Superposition Theorem Proving for Commutative Algebraic Theories
English
Universität des Saarlandes
Saarbrücken, Saarland
2000-05-25
2010-03-12
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.
expertsonly
http://edoc.mpg.de/get.epl?fid=72797&did=519771&ver=0
J.
Stuber
Jürgen
C1256104005ECAFC-38C07437FD69F7E3C1256951003719A5-Stuber1999
MPI für Informatik
Programming Logics Group
2011-07-08 13:46:57.857143
oai:edoc.mpg.de:5197722010-12-0287:932
Conference-Paper
Constraint Database Models Characterizing Timed Bisimilarity
English
Springer
Berlin, Germany
2001
2010-03-12
245
258
Las Vegas, USA
2001
Proceedings of the 3rd International Symposium on Practical Aspects of Declarative Languages
Ramakrishnan, I.V.
Lecture Notes in Computer Science
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}.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72798&did=519772&ver=0
S.
Mukhopadhyay
Supratik
A.
Podelski
Andreas
C1256104005ECAFC-BBF8B1C122A60B43C12569D000626E58-MukhopadhyayPodelski2001
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5197732010-12-0287:932
Article
On the complexity of inference about probabilistic relational models
English
2000
2010-03-12
297
308
Artificial Intelligence
117
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).
No
expertsonly
published
joureview
http://edoc.mpg.de/get.epl?fid=72799&did=519773&ver=0
M.
Jaeger
Manfred
0004-3702
C1256104005ECAFC-ADCD4005448FD8EFC12569D500647999-Jaeger00
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198122011-07-0887:932
PhD-Thesis
A Uniform Constraint-based Framework for the Verification of Infinite State Systems
English
Universität des Saarlandes
Saarbrücken, Saarland
2001-05-22
2010-03-12
expertsonly
http://edoc.mpg.de/get.epl?fid=72800&did=519812&ver=0
S.
Mukhopadhyay
Supratik
C1256104005ECAFC-01D792E063A8C408C1256A72005560AC-Mukhopadhyay-Thesis-2001
MPI für Informatik
Programming Logics Group
2011-07-08 13:13:23.870372
oai:edoc.mpg.de:5198162010-12-0287:932
Conference-Paper
The lexicographic closure as a revision process
English
?
?
2000
2010-03-12
Breckenridge, Colorado, USA
2000-04-09
2000-04-11
Proceedings of the 8th International Workshop on Non-Monotonic Reasoning (NMR 2000)
Baral, C.; Truszczynski, M.
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72801&did=519816&ver=0
http://edoc.mpg.de/get.epl?fid=72802&did=519816&ver=0
R.
Booth
Richard
http://xxx.lanl.gov/abs/cs.AI/0003017
C1256104005ECAFC-05B35447AA534C15C1256AA2003C0455-Booth2000
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198172010-12-0287:932
Conference-Paper
Constraints as Data: a New Perspective on Inferring Probabilities
English
Morgan Kaufmann
San Francisco, USA
2001
2010-03-12
755
760
Seattle, USA
2001
Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI-01)
Nebel, Bernhard
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72803&did=519817&ver=0
M.
Jaeger
Manfred
1-55860-777-3
http://www.mpi-sb.mpg.de/~jaeger/publications/IJCAI01.ps.gz
C1256104005ECAFC-BFFAFD324692662CC1256AA90049F315-JaegerIJCAI01
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198182010-12-0287:932
Article
Complex Probabilistic Modeling with Recursive Relational Bayesian Networks
English
2001
2010-03-12
179
220
Annals of Mathematics and Artificial Intelligence
32
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.
No
expertsonly
published
joureview
http://edoc.mpg.de/get.epl?fid=72804&did=519818&ver=0
M.
Jaeger
Manfred
1012-2443
C1256104005ECAFC-7C7F8A8C1C095115C1256AA9004AF849-JaegerAMAI01
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198192010-12-0287:932
Article
Automatic Derivation of Probabilistic Inference Rules
English
2001
2010-03-12
1
22
International Journal of Approximate Reasoning
1
28
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.
No
expertsonly
published
joureview
http://edoc.mpg.de/get.epl?fid=72805&did=519819&ver=0
M.
Jaeger
Manfred
0888-613X
C1256104005ECAFC-84E804A247DFE550C1256AA9004EBC08-JaegerIJAR01
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198302010-12-0287:932
Conference-Paper
A new meta-complexity theorem for bottom-up logic programs
English
Springer
Berlin, Germany
2001
2010-03-12
514
528
Siena, Italy
2001-06-18
2001-06-22
Automated reasoning : First International Joint Conference, IJCAR 2001
Goré, Rajeev; Leitsch, Alexander; Nipkow, Tobias
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72806&did=519830&ver=0
H.
Ganzinger
Harald
D.
McAllester
David
3-540-42254-4
C1256104005ECAFC-51200EE5697F66D0C1256AB5004FD735-GanzingerMcAllester-01-ijcar
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198312010-12-0287:932
Conference-Paper
Context trees
English
Springer
Berlin, Germany
2001
2010-03-12
242
256
Siena, Italy
2001-06-18
2001-06-22
Automated reasoning : First International Joint Conference, IJCAR 2001
Goré, Rajeev; Leitsch, Alexander; Nipkow, Tobias
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72807&did=519831&ver=0
H.
Ganzinger
Harald
R.
Nieuwenhuis
Robert
P.
Nivela
Pilar
3-540-42254-4
C1256104005ECAFC-EB2E979F49F72498C1256AB50052FCC3-GanzingerNieuwenhuisNivela-01-ijcar
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198322010-12-0287:932
Conference-Paper
Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems
English
IEEE
Los Alamitos, USA
2001
2010-03-12
81
90
Boston, USA
2001-06-16
2001-06-19
Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS-01)
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72808&did=519832&ver=0
H.
Ganzinger
Harald
0-7695-1281-x
C1256104005ECAFC-271953657FA398B3C1256AB50054F798-Ganzinger-01-lics
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198332010-12-0287:932
Conference-Paper
Constraints and Theorem Proving
English
Springer
Berlin, Germany
2001
2010-03-12
159
201
Gif-sur-Yvette, France
1999-08-05
1999-08-08
Contraints in Computational Logics, International Summer School (CCL-99)
Comon, Hubert; Marché, Claude; Treinen, Ralf
Lecture Notes in Computer Science
This paper is a tutorial on methods
for first-order theorem proving with constraints.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72809&did=519833&ver=0
http://edoc.mpg.de/get.epl?fid=72810&did=519833&ver=0
H.
Ganzinger
Harald
R.
Nieuwenhuis
Robert
3-540-41950-0
C1256104005ECAFC-09CCE91D7D10F1D7C1256AB5005B7F2D-GanzingerNieuwenhuis-01-ccl
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198342010-12-0287:932
Article
Automated Complexity Analysis Based on Ordered Resolution
English
2001
2010-03-12
70
109
Journal of the ACM
1
48
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.
No
expertsonly
published
joureview
http://edoc.mpg.de/get.epl?fid=72811&did=519834&ver=0
D.A.
Basin
David A.
H.
Ganzinger
Harald
C1256104005ECAFC-28522DC6EE4FC3B0C1256AB500651BA7-BasinGanzinger-01-jacm
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198382011-07-0887:932
Thesis
Ein Frontend für die Anwendung von Model Checking auf die Analyse von Array Bounds für C Programme
German
Universität des Saarlandes
Saarbrücken, Saarland
2001-04-20
2010-03-12
master
expertsonly
http://edoc.mpg.de/get.epl?fid=72812&did=519838&ver=0
G.
Jung
Georg
C1256104005ECAFC-BB14CC5B9E17DA83C1256B1A003E5478-JungDiplom2000
MPI für Informatik
Programming Logics Group
2011-07-08 12:53:40.406893
oai:edoc.mpg.de:5198402011-07-0787:932
PhD-Thesis
Einige Optimierungsmethoden hierarchischer Schaltkreise
German
Universität des Saarlandes
Saarbrücken, Saarland
2001-12-14
2010-03-12
expertsonly
http://edoc.mpg.de/get.epl?fid=72813&did=519840&ver=0
A.
Gamkrelidze
Alexander
C1256104005ECAFC-12484DF28310855CC1256B49004727A6-Gamkrelidze-Thesis-2001
MPI für Informatik
Programming Logics Group
2011-07-07 15:32:25.490519
oai:edoc.mpg.de:5198602010-12-0287:932
Conference-Paper
The Next WALDMEISTER Loop (Extended Abstract)
English
Max-Planck-Institut für Informatik
Saarbrücken, Germany
2001
2010-03-12
13
21
Havana, Cuba
2001
Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001
de Nivelle, Hans; Schulz, Stephan
Research Report
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72815&did=519860&ver=0
T.
Hillenbrand
Thomas
B.
Löchner
Bernd
C1256104005ECAFC-24C8934D9796AD20C1256B7D006E46CF-HillenbrandLoechner2001
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198642010-12-0287:932
Conference-Paper
On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results
English
Springer
Berlin, Germany
1999
2010-03-12
157
171
Trento, Italy
1999
Proceedings of the 16th International Conference on Automated Deduction (CADE-16)
Ganzinger, Harald
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72816&did=519864&ver=0
V.
Sofronie-Stokkermans
Viorica
C1256104005ECAFC-377126A3548F6E6CC12567460069F5E0-Sofronie-Stokkermans1999-cade
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
Copyright Springer
oai:edoc.mpg.de:5198722010-12-0287:932
Conference-Paper
Modeling Interaction by Sheaves and Geometric Logic
English
Springer
Berlin, Germany
1999
2010-03-12
512
523
Iasi, Romania
1999
Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99)
Ciobanu, Gabriel; Paun, Gheorghe
Lecture Notes in Computer Science
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72818&did=519872&ver=0
V.
Sofronie-Stokkermans
Viorica
K.
Stokkermans
Karel
3-540-66412-2
C1256104005ECAFC-5B6210808B8A4635C12567EE003DD107-Sofronie-Stokkermans1999-fct
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
Copyright Springer
oai:edoc.mpg.de:5198742010-12-0287:932
Conference-Paper
Resolution-based theorem proving for SHn-logics
English
Springer
Berlin, Germany
2000
2010-03-12
268
282
Vienna, Austria
2006-10-11
2006-10-11
Automated Deduction in Classical and Non-Classical Logic (Selected Papers of FTP'98)
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72821&did=519874&ver=0
V.
Sofronie-Stokkermans
Viorica
3-540-67190-0
C1256104005ECAFC-6404025BAD488864C125687A003A6AB1-Sofronie-Stokkermans-ftp2000
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
Copyright Springer
oai:edoc.mpg.de:5198782010-12-0287:932
Conference-Paper
On unification for bounded distributive lattices
English
Springer
Berlin, Germany
2000
2010-03-12
465
481
Pittsburgh, Pennsylvania, USA
2000
Proceedings of the 17th International Conference on Automated Deduction (CADE-17)
McAllester, David
Lecture Notes in Artificial Intelligence
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72822&did=519878&ver=0
V.
Sofronie-Stokkermans
Viorica
3-540-67664-3
C1256104005ECAFC-7D22049F387A3223C12568D9005867FA-Sofronie-Stokkermans-cade2000
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
Copyright Springer Verlag
oai:edoc.mpg.de:5198882010-12-0287:932
Conference-Paper
First-Order Atom Definitions Extended
English
Springer
Berlin, Germany
2001
2010-03-12
309
319
Havanna, Cuba
2001
Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001)
Nieuwenhuis, Robert; Voronkov, Andrei
Lecture Notes in Artificial Intelligence
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72823&did=519888&ver=0
B.
Afshordel
Bijan
T.
Hillenbrand
Thomas
C.
Weidenbach
Christoph
C1256104005ECAFC-A264C8F3F6DB9CF1C1256B4F004DCA17-AfshordelHillenbrandWeidenbach01
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5198952010-12-0287:932
Conference-Paper
On the Evaluation of Indexing Techniques for Theorem Proving
English
Springer
Berlin, Germany
2001
2010-03-12
257
271
Siena, Italy
2003-05-14
2003-05-18
Automated reasoning : First International Joint Conference, IJCAR 2001
Goré, Rajeev; Leitsch, Alexander; Nipkow, Tobias
Lecture Notes in Artificial Intelligence
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72825&did=519895&ver=0
R.
Nieuwenhuis
Robert
T.
Hillenbrand
Thomas
A.
Riazanov
Alexandre
A.
Voronkov
Andrei
3-540-42254-5
C1256104005ECAFC-CBAEA87E20538655C1256B7D006FC3FF-NieuwenhuisHillenbrandRiazanovVoronkov2001
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871
oai:edoc.mpg.de:5199052010-12-0287:932
Conference-Paper
Chaining Techniques for Automated Theorem Proving in Many-Valued Logics
English
IEEE
Los Alamitos, USA
2000
2010-03-12
337
344
Portland, Oregon
2003-07-08
2003-07-12
Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL-00)
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.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=72826&did=519905&ver=0
H.
Ganzinger
Harald
V.
Sofronie-Stokkermans
Viorica
0-7695-0692-5
C1256104005ECAFC-FB6D747BCE8069D1C1256743004FF6EC-GanzingerSofronie-Stokkermans-00-ismvl
MPI für Informatik
Programming Logics Group
2010-12-02 11:37:35.381871