20201022T03:40:08Zhttp://edoc.mpg.de/ac_p_oai.ploai:edoc.mpg.de:2018102010120287:932
ConferencePaper
Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER
English
Elsevier
Amsterdam, The Netherlands
2003
20040622
1
13
Valencia, Spain
20030612
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 KnuthBendix 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, setbased
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
C1256104005ECAFC13192155732F5DD1C1256D32004620FAHillenbrand2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018122010120287:932
ConferencePaper
A Principle for Incorporating Axioms into the FirstOrder Translation of Modal Formulae
English
Springer
Berlin, Germany
2003
20040617
412
426
Miami, USA
20030728
Automated deduction, CADE19 : 19th International Conference on Automated Deduction
Lecture Notes in Artificial Intelligence
In this paper we present a translation principle, called the
\emph{axiomatic translation}, for reducing propositional modal logics
with background theories, including
triangular properties such as transitivity, Euclideanness and
functionality, to decidable logics.
The goal of the axiomatic translation principle is to
find simplified theories, which
capture the inference problems in the original theory, but in a way
that is more amenable to automation and easier to deal with by existing
theorem provers.
The principle of the axiomatic translation is conceptually very simple
and can be largely automated.
Soundness is automatic under reasonable assumptions, and termination of
ordered resolution is easily achieved, but
the nontrivial part of the approach is proving completeness.
No
expertsonly
published
R.A.
Schmidt
Renate A.
U.
Hustadt
Ullrich
F.
Baader
Franz
3540405593
C1256104005ECAFC7AECA712DA7DE0B2C1256D1A005CC61ASchmidtHustadt03b
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018222010120287:932
ConferencePaper
Universal variables in disconnection tableaux
English
Springer
Berlin, Germany
2003
20040621
117
133
Rome, Italy
20030909
Automated reasoning with analytical tableaux and related methods : International Conference, TABLEAUX 2003
Lecture Notes in Artificial Intelligence
No
expertsonly
published
R.
Letz
Reinhold
G.
Stenz
Gernot
M.
Cialdea Mayer
Marta
F.
Pirri
Fiora
3540407871
C1256104005ECAFC7B50675EBAF47F08C1256EBA0047B1EALETZ03
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018232010120287:932
ConferencePaper
The New WALDMEISTER Loop at Work
English
Springer
Berlin, Germany
2003
20040623
317
321
Miami, Florida
20030728
Automated deduction, CADE19 : 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 saturationbased 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 cutdown 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 speedups. In order to minimize
communicationrelated 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
JeanMarie
T.
Hillenbrand
Thomas
B.
Löchner
Bernd
H.
Spies
Hendrik
F.
Baader
Franz
C1256104005ECAFCF7AE319E928299C3C1256D01002DD440GaillourdetHillenbrandLoechner2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018522010120287:932
ConferencePaper
Software Model Checking with Abstraction Refinement
English
Springer
Berlin, Germany
2003
20040617
1
13
New York, NY (USA)
20030109
Verification, model checking, and abstract interpretation : 4th International Conference, VMCAI 2003
Lecture Notes in Computer Science
No
expertsonly
published
A.
Podelski
Andreas
L.
Zuck
Lenore
P.
Attie
Paul
A.
Cortesi
Agostino
S.
Mukhopadhyay
Supratik
3540003487
C1256104005ECAFC2595A3BEBA35C88BC1256D0A00307971PVMCAI03
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018532010120287:932
ConferencePaper
Superposition modulo a Shostak Theory
English
Springer
Berlin, Germany
2003
20040617
182
196
Miami, Florida
20030728
Automated Deduction, CADE19 : 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 Shostakstyle 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
3540405593
C1256104005ECAFC4489C55BD13D7669C1256CFE005A7257GanzingerHillenbrandWaldmann2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018792010120287:932
Article
Orienting rewrite rules with the KnuthBendix order
English
2003
20040623
165
186
Information and Computation
183
We consider two decision problems related to the KnuthBendix order (KBO). The
first problem is \emph{orientability}: given a system of rewrite rules $R$,
does there exist an instance of KBO which orients every ground instance of
every rewrite rule in $R$. The second problem is whether a given instance of
KBO orients every ground instance of a given rewrite rule. This problem can
also be reformulated as the problem of solving a single ordering constraint for
the KBO. We prove that both problems can be
solved in the time polynomial in the size of the input.
The polynomialtime algorithm for orientability builds upon an algorithm for
solving systems of homogeneous linear inequalities over integers. We show that
the orientability problem is Pcomplete. The polynomialtime algorithm for
solving a single ordering constraint does not need to solve systems of linear
inequalities and can be run in time $O(n^2)$. Also we show that if a system is
orientable using a realvalued instance of KBO, then it is also orientable
using an integervalued instance of KBO. Therefore, all our results hold both
for the integervalued and the realvalued KBO.
No
expertsonly
published
joureview
K.
Korovin
Konstantin
A.
Voronkov
Andrei
C1256104005ECAFC989A18913FFAD6B3C1256E24003DB3B9KorovinVoronkov:IC:2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018832010120287:932
Article
Deciding the Guarded Fragments by Resolution
English
2003
20040623
21
58
Journal of Symbolic Computation
35
We give resolution based decision procedures for both
the strictly guarded fragment and the loosely guarded
fragment of firstorder logic. We prove that the
decision procedures are in 2EXPTIME, which is theoretically
optimal.
No
expertsonly
published
joureview
H.
de Nivelle
Hans
M.
de Rijke
Maarten
07477171
C1256104005ECAFC444F28344A221540C1256D0900423679deNivelle2003a
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018862010120287:932
ConferencePaper
Deciding Modal Logics through Relational Translations into GF2
English
Loria
Nancy, France
2003
20040621
15
30
Nancy, France
20030922
Proceedings of the 3rd Methods for Modalities Workshop
We provide a simple translation from the satisfiability problem for
regular grammar logics with converse into {GF2}, the intersection
of the guarded fragment and the 2variable fragment of firstorder
logic. The translation is theoretically interesting because
it translates modal logics with certain frame conditions into
firstorder logic, without explicitly expressing the frame
conditions. Using the same method, one can show that other
modal logics can be naturally translated into {GF2},
including nominal tense logics and intuitionistic propositional
logic. In our view, the results in this paper provide strong
evidence that the natural firstorder fragment corresponding
to modal logics, is {GF2}.
No
expertsonly
published
H.
de Nivelle
Hans
S.
Demri
Stéphane
C.
Areces
Carlos
P.
Blackburn
Patrick
C1256104005ECAFCB198890BD5638018C1256E270055D64FdeNivelleDemri2003c
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018942010120287:932
Article
On Using Ground Joinable Equations in Equational Theorem Proving
English
2003
20040623
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 \ACoperators we present a simple redundancy
criterion which is easy to implement, efficient, and effective in
practice, leading to significant speedups.
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
07477171
C1256104005ECAFCA129A5E170AD94F0C1256D01002C84B9AvenhausHillenbrandLoechner2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018972010120287:932
ConferencePaper
ACcompatible KnuthBendix Order
English
Springer
Berlin, Germany
2003
20040623
47
59
Miami, Florida
20030514
Automated deduction, CADE19 : 19th International Conference on Automated Deduction
Lecture Notes in Computer Science
We introduce a family of ACcompatible KnuthBendix simplification orderings
which are ACtotal on ground terms.
Our orderings preserve attractive features of
the original KnuthBendix orderings
such as polynomial algorithm for comparing terms; the orderings admit
computationally efficient approximations
like checking weights of terms;
and prefer light terms to heavy ones.
This makes them especially suited for automated deduction
where efficient treatment of orderings is desirable.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=9154&did=201897&ver=0
K.
Korovin
Konstantin
A.
Voronkov
Andrei
F.
Baader
Franz
C1256104005ECAFC7B6594FD381CBD9AC1256D170068CDF9KorovinVoronkov:CADE03:ACKBO
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2018992010120287:932
InBook
Representation Theorems and the Semantics of Nonclassical Logics, and Applications to Automated Theorem Proving
English
Springer
Berlin, Germany
2003
20040617
59
100
114
Beyond Two: Theory and Applications of Multiple Valued Logic
Fitting, Melvin; Orlowska, Ewa
We give a uniform presentation of representation and
decidability results related to the Kripkestyle
semantics of several nonclassical logics.
We show that a general representation theorem
(which has as particular instances the representation
theorems as algebras of sets for Boolean algebras,
distributive lattices and semilattices)
extends in a natural way to several classes of operators
and allows to establish a relationship between algebraic
and Kripkestyle models. We illustrate the ideas on several examples.
We conclude by showing how the Kripkestyle models thus obtained can be used
(if firstorder axiomatizable) for automated theorem proving by
resolution for some nonclassical logics.
No
expertsonly
published
notspecified
http://edoc.mpg.de/get.epl?fid=9156&did=201899&ver=0
V.
SofronieStokkermans
Viorica
M.
Fitting
Melvin
E.
Orlowska
Ewa
3790815411
C1256104005ECAFCF6DA8B3F1A74700FC1256BBC003EC55CSofronieStokkermansmvl2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
Copyright Springer Verlag.
oai:edoc.mpg.de:2019032010120287:932
ConferencePaper
Orienting Equalities with the KnuthBendix Order
English
IEEE
Los Alamitos, USA
2003
20040623
75
84
Ottawa, Canada
20030708
18th Annual IEEE Symposium on Logic in Computer Science (LICS03)
Orientability of systems of equalities is the following
problem: given a system of equalities $s_1 \eql t_1, \ldots,
s_n \eql t_n$, does there exist a simplification ordering $\succ$
which orients the system,
that is for every $i \in \{1,...,n\}$,
either $s_i \succ t_i$ or $t_i \succ s_i$.
This problem can be used in rewriting for finding
a canonical rewrite system for a system of equalities
and in theorem proving for adjusting simplification
orderings during completion. We prove that (rather surprisingly)
the problem can be solved in polynomial time when we restrict ourselves to the
KnuthBendix orderings.
No
expertsonly
published
http://edoc.mpg.de/get.epl?fid=9157&did=201903&ver=0
K.
Korovin
Konstantin
A.
Voronkov
Andrei
P.
Kolaitis
Phokion
C1256104005ECAFC82F4C113C50FFB4CC1256D1700657425KorovinVoronkov:LICS03:EqOrientability
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2019092010120287:932
Article
Resolutionbased decision procedures for the universal theory of some classes of distributive lattices with operators
English
2003
20040617
891
924
Journal of Symbolic Computation
36
We establish a link between the satisfiability of universal
sentences with respect to classes of distributive lattices
with operators and their satisfiability with respect to
certain classes of relational structures.
This justifies a method for structurepreserving translation
to clause form of universal sentences in such classes of
algebras.
We show that refinements of resolution yield decision procedures
for the universal theory of some such classes. In particular, we
obtain exponential space and time decision procedures
for the universal clause theory of
(i) the class of all bounded distributive lattices with
operators satisfying a set of (generalized) residuation
conditions,
(ii) the class of all bounded distributive lattices with
operators,
and a doublyexponential time decision procedure for the
universal clause theory of the class of all Heyting algebras.
No
expertsonly
published
joureview
http://edoc.mpg.de/get.epl?fid=9158&did=201909&ver=0
V.
SofronieStokkermans
Viorica
07477171
C1256104005ECAFCCEC92761F334BFFAC1256CB50050C081SofronieStokkermansjsc2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
Copyright Elsevier Publishers
oai:edoc.mpg.de:2019822010120287:932
Article
Boolean and Cartesian Abstraction for Model Checking C Programs
English
2003
20040623
1
15
International Journal on Software Tools for Technology Transfer (STTT)
5
Automatic journal name synchronization
No
expertsonly
published
joureview
A.
Podelski
Andreas
T.
Ball
Tom
S.K.
Rajamani
Sriram K.
14332779
C1256104005ECAFC4BE46022487BA706C1256D0A00322329BPRSTTT03
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2019832010120287:932
ConferencePaper
Verification of Cryptographic Protocols: Tagging Enforces Termination
English
Springer
Berlin, Germany
2003
20040629
136
152
Warsaw, Poland
20030407
Foundations of software science and computation structures : 6th International Conference, FOSSACS 2003
Lecture Notes in Computer Science
No
expertsonly
published
notspecified
B.
Blanchet
Bruno
A.
Podelski
Andreas
A.D.
Gordon
Andrew D.
3540008977
C1256104005ECAFC882EFCF8FCEA7F73C1256D0A0030D9D3BPFossacs03
MPI für Informatik
Programming Logics Group
MPI für Informatik
Static Analysis Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020192010120287:932
ConferencePaper
New Directions in InstantiationBased Theorem Proving
English
IEEE
Los Alamitos, USA
2003
20040617
55
64
Ottawa, Canada
20030622
18th Annual IEEE Symposium on Logic in Computer Science (LICS03)
We consider instantiationbased 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
firstorder 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
0769518842
C1256104005ECAFC9F899010FD50E7D7C1256D170066FF4BGanzingerKorovin03lics
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020212010120287:932
ConferencePaper
Solving Existentially Quantified Constraints with One Equality and Arbitrarily Many Inequalities
English
Springer
Berlin, Germany
2003
20040617
615
633
Kinsale, Ireland
20030929
Principles and practice on constraint programming  CP 2003 : 9th International Conference, CP 2003
Lecture Notes in Computer Science
This paper contains the first algorithm that can solve disjunctions of
constraints of
the form $\exists\SVec{y}\STI B \; [ f=0 \;\wedge\; g_1\geq
0\wedge\dots\wedge g_k\geq 0
]$ in free variables $\SVec{x}$, terminating for all cases when this results
in a numerically
wellposed problem. Here the only assumption on the terms $f, g_1,\dots, g_n$
is the
existence of a pruning function, as given by the usual constraint propagation
algorithms
or by interval evaluation. The paper discusses the application of an
implementation of
the resulting algorithm on problems from control engineering, parameter
estimation, and computational geometry.
No
expertsonly
published
S.
Ratschan
Stefan
F.
Rossi
Francesca
C1256104005ECAFC9C2FFBD5E650EE93C1256DD500366F0ERatschan2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020232010120287:932
ConferencePaper
Probabilistic Classifiers and the Concepts they Recognize
English
AAAI Press
Menlo Park, USA
2003
20040623
266
273
Washington DC, U.S.
20030821
Proceedings of the Twentieth International Conference on Machine Learning (ICML03)
We investigate algebraic, logical, and geometric
properties of concepts recognized by various classes
of probabilistic classifiers. For this we introduce a
natural hierarchy of probabilistic classifiers, the
lowest level of which comprises the naive Bayesian
classifiers. We show that the expressivity of classifiers on the
different levels in the hierarchy is characterized
algebraically by separability with polynomials of
different degrees. A consequence of this result is that
every linearly separable concept can be recognized by a
naive Bayesian classifier. We contrast this result with
negative results about the naive Bayesian classifier
previously reported in the literature, and point out that
these results only pertain to specific learning
scenarios for naive Bayesian classifiers. We also present
some logical and geometric characterizations of linearly
separable concepts, thus providing additional intuitive
insight into what concepts are recognizable by naive
Bayesian classifiers.
No
expertsonly
published
M.
Jaeger
Manfred
T.
Fawcett
Tom
N.
Mishra
Nina
01577351894
C1256104005ECAFC6343C6DE715C6629C1256D23004B9A2BJaegerICML03
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020262010120287:932
ConferencePaper
A Representation Theorem and Applications
English
Springer
Berlin, Germany
2003
20040617
50
61
Aalborg, Denmark
20030702
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 equivariancebased 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.
3540404945
C1256104005ECAFC8F468E8BDA25A19FC1256D01002C63A8JaegerECSQARU03
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020272010120287:932
ConferencePaper
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
English
Springer
Berlin, Germany
2003
20040617
335
349
Miami, Florida
20030728
Automated Deduction, CADE19 : 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
3540405593
C1256104005ECAFC834A2D263C7BFE3F00256D200035E7D7GanzingerStuber2003cade
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020292010120287:932
ConferencePaper
Implementing the clausal normal form transformation with proof generation
English
University of Liverpool, University of Manchester
Liverpool, UK
2003
20040621
69
83
Almaty, Kazachstan
20030925
Fourth Workshop on the Implementation of Logics
We explain how to implement the clausal normal form transformation
with proof generation. We present
a convenient data structure for sequent calculus proofs, which
will be used for representing the generated proofs.
The data structure allows easy proof checking and generation
of proofs. In addition, it allows
convenient implementation of proof normalization, which is necessary
in order to keep the size of the generated proofs acceptable.
No
expertsonly
published
H.
de Nivelle
Hans
B.
Konev
Boris
R.
Schmidt
Renate
C1256104005ECAFCFB577616A96B276BC1256E270056CE80deNivelle2003c
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020302010120287:932
ConferencePaper
Automated theorem proving by resolution in nonclassical logics
English
INRIA
Domaine de Voulceau  Rocquencourt, France
2003
20040622
151
167
Metz, France
20030903
Fourth International Conference Journees de l'Informatique Messine: Knowledge Discovery and Discrete Mathematics (JIM03)
We present several classes of nonclassical logics
(many of which are practically relevant in knowledge
representation)
which can be translated into tractable and relatively
simple fragments of classical logic.
In this context, refinements of resolution can be often
used successfully for automated theorem proving, and
in many cases yield optimal decision procedures.
No
expertsonly
published
V.
SofronieStokkermans
Viorica
M.
Nadif
Mohamed
A.
Napoli
Amedeo
E.
SanJuan
Eric
A.
Sigayret
Alain
2726112560
C1256104005ECAFC7C3D3A23074C8A17C1256D9D00366F25SofronieStokkermansjim2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020312010120287:932
Article
Model checking mobile ambients
English
2003
20040617
277
331
Theoretical Computer Science
308
We settle the complexity bounds of the model checking problem for the ambient
calculus with public names against the ambient logic. We show that if either
the calculus contains replication or the logic contains the guarantee operator,
the problem is undecidable. In the case of the replicationfree calculus and
guaranteefree logic we prove that the problem is PSPACEcomplete. For the
complexity upperbound, we devise a new representation of processes that
remains of polynomial size during process execution; this allows us to keep the
model checking procedure in polynomial space. Moreover, we prove
PSPACEhardness of the problem for several quite simple fragments of the
calculus and the logic; this suggests that there are no interesting fragments
with polynomialtime model checking algorithms.
No
expertsonly
published
joureview
W.
Charatonik
Witold
S.
Dal Zilio
Silvano
A.D.
Gordon
Andrew Donald
S.
Mukhopadhyay
Supratik
J.M.
Talbot
JeanMarc
03043975
C1256104005ECAFC30C5005D9C1C805CC1256D200054C703CharatonikDGMT2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020322010120287:932
ConferencePaper
Subsumption of Concepts in FL_0 for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACEcomplete
English
CEUR
Aachen, Germany
2003
20040622
56
64
Rome, Italy
20030905
2003 International Workshop on Description Logics (DL03)
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 PSPACEcomplete for descriptive
semantics when cyclic definitions are allowed. Our proof uses automata theory
and as a byproduct we establish the PSPACEcompleteness 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
16130073
C1256104005ECAFC746B1C632282C1C9C1256E23006ADC00Kazakov03SubsumptionFLzero
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020452010120287:932
ConferencePaper
Translation of Resolution Proofs into Short FirstOrder Proofs without Choice Axioms
English
Springer
Berlin, Germany
2003
20040617
365
379
Miami, USA
20030728
Automated deduction, CADE19 : 19th International Conference on Automated Deduction
Lecture Notes in Artificial Intelligence
We present a way of transforming a resolution proof containing
Skolemization into a natural deduction proof of the same formula
but not using Skolemization. The size of the
proof increases only moderately (polynomially).
This makes it possible to translate the output of a resolution
theorem prover into a purely firstorder proof that is moderate
in size.
No
expertsonly
published
H.
de Nivelle
Hans
F.
Baader
Franz
3540405593
C1256104005ECAFC179628522133A695C1256D0A0041B7F3deNivelle2003b
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020482010120287:932
ConferencePaper
Compositional Circular AssumeGuarantee Rules Cannot Be Sound and Complete
English
Springer
Berlin, Germany
2003
20040617
343
357
Warsaw, Poland
20030407
Foundations of software science and computation structures : 6th International Conference, FOSSACS 2003
Lecture Notes in Computer Science
Circular assumeguarantee reasoning is used for the compositional verification
of concurrent systems. Its soundness has been studied in depth, perhaps because
circularity makes it anything but obvious. In this paper, we investigate
completeness. We show that compositional circular assumeguarantee rules cannot
be both sound and complete.
No
expertsonly
published
P.
Maier
Patrick
A.D.
Gordon
Andrew D.
3540008977
C1256104005ECAFCD6DFA25A621ED297C1256D08004352DEMaier2003
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020522010120287:932
Article
Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II)
English
2002
20030729
831
861
Journal of Symbolic Computation
33
Cancellative superposition is a refutationally complete
calculus for firstorder equational theorem proving in the
presence of the axioms of cancellative abelian monoids, and,
optionally, the torsionfreeness axioms. Thanks to strengthened
ordering restrictions, cancellative superposition avoids some
of the inefficiencies of classical ACsuperposition calculi.
We show how the efficiency of cancellative superposition can
be further improved by using variable elimination techniques,
leading to a significant reduction of the number of variable
overlaps. In particular, we demonstrate that in divisible
torsionfree abelian groups, variable overlaps, ACunification
and ACorderings can be avoided completely.
No
expertsonly
published
joureview
U.
Waldmann
Uwe
07477171
C1256104005ECAFCB3DB8397B9661C6DC1256CAE005B88DBWaldmann2002bJSC
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2020902010120287:932
ConferencePaper
FiniteControl Mobile Ambients
English
Springer
Berlin, Germany
2002
20030901
295
313
Grenoble, France
20020408
Programming languages and systems: 11th European Symposium on Programming, ESOP 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002
Lecture Notes in Computer Science
We define a finitecontrol fragment of the ambient calculus, a
formalism for describing distributed and mobile computations. A
series of examples demonstrates the expressiveness of our fragment. In
particular, we encode the choicefree, finitecontrol, synchronous
$\pi$calculus. We present an algorithm for model checking this fragment
against the ambient logic (without composition adjunct). This is the first
proposal of a model checking algorithm for ambients to deal with
recursivelydefined, possibly nonterminating, processes. Moreover, we show
that the problem is PSPACEcomplete, like other fragments considered in the
literature. Finitecontrol versions of other process calculi are obtained via
various syntactic restrictions. Instead, we rely on a novel type system that
bounds the number of active ambients and outputs in a process; any typable
process has only a finite number of derivatives.
No
expertsonly
published
notspecified
W.
Charatonik
Witold
A.D.
Gordon
Andrew Donald
J.M.
Talbot
JeanMarc
D.
Le Métayer
Daniel
3540433635
C1256104005ECAFC585F3CCBCA901996C1256C4100675599CharatonikGT2002
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021012010120287:932
ConferencePaper
Shostak Light
English
Springer
Heidelberg, Germany
2002
20030901
332
346
Copenhagen, Denmark
20020727
Automated deduction, CADE18 : 18th International Conference on Automated Deduction
Lecture Notes in Artificial Intelligence
We represent the essential ingredients of Shostak's procedure at a high level
of abstraction, and as a refinement of the NelsonOppen procedure. We analyze
completeness issues of the method based on a general notion of theories. We
also formalize a notion of sigmamodels and show that on the basis of Shostak's
procedure we cannot distinguish a theory from its approximation represented by
the class of its sigmamodels.
No
expertsonly
published
notspecified
H.
Ganzinger
Harald
A.
Voronkov
Andrei
3540439315
C1256104005ECAFC332756F3E18C6188C1256BBB0045CB5CGanzinger02cade
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021022010120287:932
ConferencePaper
Context trees
English
Springer
Berlin, Germany
2001
20030901
242
256
Siena, Italy
20010618
Automated reasoning : First International Joint Conference, IJCAR 2001
Lecture Notes in Artificial Intelligence
Indexing data structures are wellknown to be crucial for the
efficiency of the current stateoftheart 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
stateoftheart implementations of the other main techniques.
In particular space consumption of context trees
is substantially less than for other index structures.
No
expertsonly
published
notspecified
H.
Ganzinger
Harald
R.
Nieuwenhuis
Robert
P.
Nivela
Pilar
R.
Goré
Rajeev
A.
Leitsch
Alexander
T.
Nipkow
Tobias
3540422544
C1256104005ECAFCEB2E979F49F72498C1256AB50052FCC3GanzingerNieuwenhuisNivela01ijcar
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021032010120287:932
ConferencePaper
Extraction of Proofs from the Clausal Normal Form Transformation
English
Springer
Berlin, Germany
2002
20030804
584
598
Edinburgh, UK
20020922
Computer Science Logic : 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL
Lecture Notes in Computer Science
We give techniques for extracting proofs from the
Clausal Normal Form transformation. We discuss and solve three
technical problems:
{\bf (1)}. How to handle the introduction of definitions and Skolem functions.
{\bf (2)}. How to generate short (linear size) proofs.
{\bf (3)}. How to handle optimized Skolemization. We reduce it
to standard Skolemization.
No
expertsonly
published
notspecified
H.
de Nivelle
Hans
J.
Bradfield
Julian
3540442405
C1256104005ECAFC9D6F3F8E8C3039C0C1256D090039E7D0deNivelle2002a
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021072010120287:932
ConferencePaper
Probababilistic Decision Graphs  Combining Verification and AI Techniques for Probabilistic Inference
English
Computer Science Department, University of Castilla  La Mancha

2002
20030812
81
88
Cuenca, Spain
20021106
Proceedings of the First European Workshop on Probabilistic Graphical Models
We adopt probabilistic decision graphs developed in the
field of automated verification as a tool for probabilistic model
representation and inference.
We show that probabilistic inference has linear time complexity in
the size of the probabilistic decision graph, that the smallest
probabilistic decision graph for a given distribution is at most
as large as the smallest junction tree for the same distribution,
and that in some cases it can in fact be much smaller.
Behind these very promising features of probabilistic decision graphs
lies the fact that they integrate into a single coherent framework
a number of representational
and algorithmic optimizations
developed for Bayesian networks (use of hidden variables, contextspecific
independence, structured representation of conditional probability tables).
No
expertsonly
published
notspecified
M.
Jaeger
Manfred
C1256104005ECAFC8B96E7D1BCDFF6ECC1256CAF00678172JaegerPGM02
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021082010120287:932
ConferencePaper
Is Logic Effective for Analyzing C Programs?
English
MaxPlanckInstitut für Informatik
Saarbrücken, Germany
2002
20030901
27
30
Saarbrücken
20020304
Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi
MPI Research Report
No
expertsonly
published
notspecified
T.
Hillenbrand
Thomas
A.
Podelski
Andreas
D.
Topić
Dalibor
W.
Charatonik
Witold
H.
Ganzinger
Harald
C1256104005ECAFC87105CCDA5C457F0C1256B9C00512EAAHPT02
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021092010120287:932
ConferencePaper
The Next WALDMEISTER Loop
English
Springer
Heidelberg, Germany
2002
20030901
486
500
Copenhagen, Denmark
20020727
Automated deduction, CADE18 : 18th International Conference on Automated Deduction
Lecture Notes in Artificial Intelligence
In saturationbased theorem provers, the reasoning process consists
in constructing the closure of an axiom set under inferences. As is
wellknown, this process tends to quickly fill the memory available
unless preventive measures are employed. For implementations based
on the DISCOUNT loop, the passive facts are responsible for most
of the memory consumption. We present a refinement of that loop
allowing such a compression that the space needed for the passive
facts is linearly bound by the number of active facts. In practice,
this will reduce memory consumption in the WALDMEISTER system by
more than one order of magnitude as compared to previous compression
schemes.
No
expertsonly
published
notspecified
T.
Hillenbrand
Thomas
B.
Löchner
Bernd
A.
Voronkov
Andrei
3540439315
C1256104005ECAFCE2D2AE34E6600015C1256CB7005419D1HL02CADE18
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021102010120287:932
ConferencePaper
Relating Semantic and ProofTheoretic Concepts for Polynomial Time Decidability of Uniform Word Problems
English
IEEE
Los Alamitos, USA
2001
20030812
81
90
Boston, USA
20010616
Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS01)
In this paper we compare three approaches
to polynomial time decidability
for uniform word problems for quasivarieties.
Two of the approaches,
by Evans and Burris, respectively, are semantical, referring to
certain embeddability and axiomatizability properties.
The third approach is prooftheoretic 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
notspecified
H.
Ganzinger
Harald
D.A.
Williams
Denise A.
076951281x
C1256104005ECAFC271953657FA398B3C1256AB50054F798Ganzinger01lics
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021152010120287:932
Article
Resolution in modal, description and hybrid logic
English
2001
20030901
717
736
Journal of Logic and Computation
11
No
expertsonly
published
joureview
C.
Areces
Carlos
M.
de Rijke
Maarten
H.
de Nivelle
Hans
0955792X
C1256104005ECAFCA98D062B6D5E6E9D00256D20004EEDCCArecesRijkeNivelle02
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021192010120287:932
ConferencePaper
Compositional Termination Analysis of Symbolic Forward Analysis
English
Springer
Berlin, Germany
2002
20030804
109
125
Venice, Italy
20020121
Verification, Model Checking, and Abstract Interpretation. Third International Workshop, VMCAI 2002
Lecture Notes in Computer Science
Existing model checking tools for infinite state systems, such as
UPPAAL, HYTECH and KRONOS, use symbolic forward analysis, a possibly
nonterminating procedure. We give termination criteria that allow us to
reason compositionally about systems defined with asynchronous parallel
composition; we can prove the termination of symbolic forward analysis for a
composed system from the syntactic conditions satisfied by the component
systems.
Our results apply to nonlinear hybrid systems; in particular to
rectangular hybrid systems, timed automata and ominimal systems. In the case
of integervalued systems we give negative results: forward analysis is not
wellsuited for this class of initestate systems.
No
expertsonly
published
notspecified
W.
Charatonik
Witold
S.
Mukhopadhyay
Supratik
A.
Podelski
Andreas
A.
Cortesi
Agostino
3540436316
C1256104005ECAFC978EDB9065F405D7C1256C41006672B0CharatonikMP2002
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021202010120287:932
ConferencePaper
On Name Generation and SetBased Analysis in the DolevYao Model
English
Springer
Berlin, Germany
2002
20030901
499
514
Brno, Czech Republic
20020820
CONCUR 2002  Concurrency Theory. 13th International Conference
Lecture Notes in Computer Science
We study the control reachability problem in the DolevYao model of
cryptographic protocols when principals are represented by tail recursive
processes with generated names. We propose a conservative approximation of the
problem by reduction to a nonstandard collapsed operational semantics and we
introduce checkable syntactic conditions entailing the equivalence of the
standard and the collapsed semantics. Then we introduce a conservative and
decidable setbased analysis of the collapsed operational semantics and we
characterize a situation where the analysis is exact.
No
expertsonly
published
notspecified
W.
Charatonik
Witold
R.
Amadio
Roberto
L.
Brim
Lubos
P.
Jancar
Petr
M.
Kretinsky
Mojomir
A.
Kucera
Antonin
3540440437
C1256104005ECAFC9CAB51ABF47485F7C1256C410069794BAmadioCharatonik2002
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021212010120287:932
Article
Automated Proof Construction in Type Theory using Resolution
English
2002
20030901
253
275
Journal of Automated Reasoning
29
We provide techniques to integrate resolution logic with equality
in type theory. The results may be rendered as follows:
{\bf (1)}. A clausification procedure in type theory, equipped with
a correctness proof, all encoded using higherorder primitive recursion.
{\bf (2)}. A novel representation of clauses in minimal logic
such that the $ \lambda $representation of resolution steps
is linear in the size of the premisses.
{\bf (3)}. Availability of the power of resolution theorem provers in
interactive proof construction systems based on
type theory.
No
expertsonly
published
joureview
M.
Bezem
Marc
D.
Hendriks
Dimitri
H.
de Nivelle
Hans
01687433
C1256104005ECAFCB231DAC4BCC58595C1256D090040A825deNivelle2002b
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021222010120287:932
InBook
Logical Frameworks
English
Reidel
Dordrecht, The Netherlands
2002
20030723
89
164
9
Handbook of Philosophical Logic
Gabbay, Dov;Guenthner, Franz
No
expertsonly
published
notspecified
D.A.
Basin
David A.
S.
Matthews
Sean
D.
Gabbay
Dov
F.
Guenthner
Franz
1402006993
C1256104005ECAFCAEF8AFC876CFBE63C12568B20047B9DABasinMatthewsHPL
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021232010120287:932
Article
Automated Complexity Analysis Based on Ordered Resolution
English
2001
20030901
70
109
Journal of the ACM
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 nonlocal 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 coNP.
No
expertsonly
published
joureview
D.A.
Basin
David A.
H.
Ganzinger
Harald
C1256104005ECAFC28522DC6EE4FC3B0C1256AB500651BA7BasinGanzinger01jacm
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021272010120287:932
ConferencePaper
ConstraintBased Infinite Model Checking and Tabulation for Stratified CLP
English
Springer
Berlin, Germany
2002
20030811
115
129
Copenhagen, Denmark
20020729
Logic Programming. 18th International Conference, ICLP 2002
Lecture Notes in Computer Science
Forward analysis procedures for infinitestate systems such as timed systems
were limited to safety properties. We give the first constraintbased forward
analysis for infinitestate systems that goes beyond safety properties. Namely,
we take the restriction of the $\mu$calculus to leastfixpoint formulas where
negation is applied to closed subformulas only. We characterize these
properties as perfect models of constraint logic programs, and we present a
tabulation procedure for the topdown evaluation of stratified constraint logic
programs.
No
expertsonly
published
notspecified
W.
Charatonik
Witold
S.
Mukhopadhyay
Supratik
A.
Podelski
Andreas
P.J.
Stuckey
Peter J.
3540439307
C1256104005ECAFC6DEE3A59494DC2A5C1256CB70052FB4ACharatonikMP2002a
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021332010120287:932
ConferencePaper
Atomic Set Constraints with Projection
English
Springer
Berlin, Germany
2002
20030901
311
325
Copenhagen, Denmark
20020722
Rewriting Techniques and Applications. 13th International Conference, RTA 2002
Lecture Notes in Computer Science
We investigate a class of set constraints defined as atomic set
constraints augmented with projection. This class subsumes some
already studied classes such as atomic set constraints with
lefthand side projection and INES constraints. All these classes
enjoy a nice property that satisfiability can be performed in cubic time. This
has be contrasted with several other classes of set constraints, such as
definite set constraints and positive set constraints, for which
satisfiability ranges from DEXPTIMEcomplete to NEXPTIMEcomplete. However,
these latter classes allow set operators such as intersection or union which
is not the case for the class studied here. In the case of atomic set
constraints with projection one might expect that satisfiability remains
polynomial. Unfortunately, we show that that the satisfiability problem for
this class is no longer polynomial, but CoNPhard. Furthermore, we devise a
PSPACE algorithm to solve this satisfiability problem.
No
expertsonly
published
notspecified
W.
Charatonik
Witold
J.M.
Talbot
JeanMarc
S.
Tison
Sophie
354043916
C1256104005ECAFC4F68EEC65F1C33B1C1256C410067F53CCharatonikTalbot2002
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021342010120287:932
Article
Set Constraints with Intersection
English
2002
20030509
213
229
Information and Computation
179
Set constraints are inclusions between expressions denoting sets of
trees (over a given alphabet of constructor symbols). The
efficiency of their satisfiability test is a central issue in
setbased program analysis, their main application domain. We
introduce the class of {\em set constraints with intersection}\/
(the only operators forming the expressions are constructors and
intersection) and show that its satisfiability problem is
DEXPTIMEcomplete. This is the first class of set constraints (over
a general constructor alphabet) that falls into this complexity
class. The solved form in our algorithm represents the least
solution as a tree automaton and exhibits which variables denote the
empty set. We furthermore prove that set constraints with
intersection are equivalent to {\em definite set constraints}\/ (in
expressive power, and the satisfiability problems are linearly
interreducible). The class of definite set constraints was the
first one for which the decidability question was solved; we hereby
settle also the complexity question.
No
expertsonly
published
joureview
W.
Charatonik
Witold
A.
Podelski
Andreas
08905401
C1256104005ECAFC079D7DD74FCAD6F6412566FD0057B689CPintersectionJ
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021362010120287:932
Proceedings
Deduction
English
IBFI
Wadern, Germany
2000
20030901
Wadern/Dagstuhl, Germany
19990228
No
expertsonly
published
U.
Furbach
Ulrich
H.
Ganzinger
Harald
R.
Hasegawa
Ryuzo
D.
Kapur
Deepak
09401121
C1256104005ECAFC32CB6BDB1284186CC12569F2004C0200Ganzingeretal01Dagstuhl
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021372010120287:932
ConferencePaper
0/1 Optimization and 0/1 Primal Separation are Equivalent
English
ACM SIAM
New York, Philadelphia, USA
2002
20030901
920
926
San Francisco, USA
20020106
Proceedings of the 13th Annual ACM SIAM Symposium on Discrete Algorithms
No
expertsonly
published
notspecified
F.
Eisenbrand
Friedrich
G.
Rinaldi
Giovanni
P.
Ventura
Paolo
C1256104005ECAFC5E03EA9A054B3B09C1256B96002CAE90ERV02
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021382010120287:932
ConferencePaper
A Theory of Inductive Query Answering
English
IEEE
Los Alamitos, USA
2002
20030901
123
130
Maebashi City, Japan
20021209
Proceedings of the 2002 IEEE International Conference on Data Mining (ICDM'02)
We introduce the boolean inductive query evaluation problem, which is
concerned with answering inductive que
ries
that are arbitrary boolean expressions over monotonic and antimonotonic
predicates. Secondly, we develop a d
ecomposition theory for inductive query evaluation in which
a boolean query $Q$ is reformulated into $k$ subqueries $Q_i = Q_A \wedge Q_M$
that are the conjunction of a
monotonic and an antimonotonic predicate.
The solution to each subquery can be represented using a version space.
We investigate how the number of version spaces $k$ needed to answer the query
can be minimized.
Thirdly, for the pattern domain of strings, we show how the version spaces can
be represented using a novel
data structure, called the version space tree, and can be computed using a
variant of the famous Apriori alg
orithm.
Finally, we present some experiments that validate the approach.
No
expertsonly
published
notspecified
L.
de Raedt
Luc
M.
Jaeger
Manfred
S.D.
Lee
Sau Dan
H.
Mannila
Heikki
0769517544
C1256104005ECAFCE441266330064017C1256CAF00665F14deRJaeLeeMan02
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021392010120287:932
Proceedings
Proceedings of the 2nd International Workshop on the Implementation of Logics
English
MaxPlanckInstitut für Informatik
Saarbrücken, Germany
2001
20030901
Havanna, Cuba
20011208
No
expertsonly
published
H.
de Nivelle
Hans
S.
Schulz
Stephan
0946011X
C1256104005ECAFC85B5D5861A15681BC1256B84004FB61DdeNivelleSchulz2001
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021402010120287:932
ConferencePaper
Logical Algorithms
English
Springer
Berlin, Germany
2002
20030901
209
223
Copenhagen, Denmark
20020729
Logic Programming. 18th International Conference, ICLP 2002
Lecture Notes in Computer Science
It is widely accepted that many algorithms can be concisely and clearly
expressed as logical inference rules. However, logic programming has been
inappropriate for the study of the running time of algorithms because there has
not been a clear and precise model of the run time of a logic program. We
present a logic programming model of computation appropriate for the study of
the run time of a wide variety of algorithms.
No
expertsonly
published
notspecified
H.
Ganzinger
Harald
D.
McAllester
David
P.J.
Stuckey
Peter J.
3540439307
C1256104005ECAFC579C0AB32F1BD048C1256C410068CB89GanzingerMcAllester02iclp
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021412010120287:932
ConferencePaper
A new metacomplexity theorem for bottomup logic programs
English
Springer
Berlin, Germany
2001
20030901
514
528
Siena, Italy
20010618
Automated reasoning : First International Joint Conference, IJCAR 2001
Lecture Notes in Artificial Intelligence
Nontrivial
metacomplexity theorems, proved once for a programming language
as a whole, facilitate the presentation and analysis
of particular algorithms. This paper gives a new
metacomplexity theorem
for bottomup logic programs
that is both more general and more accurate
than previous such theorems.
The new theorem applies to algorithms
not handled by previous metacomplexity theorems,
greatly facilitating their analysis.
No
expertsonly
published
notspecified
H.
Ganzinger
Harald
D.
McAllester
David
R.
Goré
Rajeev
A.
Leitsch
Alexander
T.
Nipkow
Tobias
3540422544
C1256104005ECAFC51200EE5697F66D0C1256AB5004FD735GanzingerMcAllester01ijcar
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021422010120287:932
InBook
A ResolutionBased Decision Procedure for Extensions of K4
English
CSLI
Stanford, USA
2001
20030728
225
246
119
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 wellstructured clauses
closed under ordered resolution and negative chaining.
No
expertsonly
published
notspecified
H.
Ganzinger
Harald
U.
Hustadt
Ullrich
C.
Meyer
Christoph
R.A.
Schmidt
Renate A.
M.
Zakharyaschev
Michael
K.
Segerberg
Krister
M.
de Rijke
Maarten
H.
Wansing
Heinrich
1575862727
C1256104005ECAFC0BECC945CC71EA19C125675A006045A2Ganzingeretal00AIML
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021432010120287:932
Article
Efficient deductive methods for program analysis
English
2001
20030728
102
103
ACM SIGPLAN Notices
36
Automatic journal name synchronization
No
expertsonly
published
joureview
H.
Ganzinger
Harald
03621340
C1256104005ECAFCD3A03BCFE06E5150C1256B44005E1BD2Ganzinger:2001:EDM
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021442010120287:932
Article
A Phytography of WALDMEISTER
English
2002
20030729
127
133
AI Communications
15
The architecture of the {Waldmeister} prover for unit equational
deduction is based on a strict separation of active and passive
facts. After an inspection of the system's proof procedure, the
representation of each of the central data structures is outlined,
namely indexing for the active facts, compression for the passive
facts, successor sets for the hypotheses, and minimal recording of
inference steps for the proof object. In order to cope with large
search spaces, specialized redundancy criteria are employed, and the
empirically gained control knowledge is integrated to ease the use
of the system. The paper concludes with a quantitative comparison of
the {Waldmeister} versions over the years, and a view of the future
prospects.
No
expertsonly
published
joureview
B.
Löchner
Bernd
T.
Hillenbrand
Thomas
09217126
C1256104005ECAFC4116BB9292AC8F43C1256C1D0040D29DLoechnerHillenbrandAICOM2002
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021452010120287:932
Article
Utilitarian Desires
English
2002
20030729
329
363
Autonomous Agents and MultiAgent Systems
5
No
expertsonly
published
joureview
J.
Lang
Jérôme
L.W.N.
van der Torre
Leendert W. N.
E.
Weydert
Emil
13872532
C1256104005ECAFC49D842536433ECB4C1256A00006FF4B1Weydert2001f
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021462010120287:932
ConferencePaper
Recursive resolution for modal logic
English
MaxPlanckInstitut für Informatik
Saarbrücken, Germany
2002
20030901
11
15
Saarbrücken, Germany
20020304
Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi
MPI Research Report
Resolution for the first order logic can be considered as a
practical tool for obtaining a decision procedures for some
theories (cf. \cite{arm}). For modal logics, however, there is
no uniform formulation of the resolution principle, yet the normal modal
logics are the most probable candidates to be decidable
theories. The translational methods for modal logic, treated for
instance in \cite{ohl}, yet possess some uniformness property, but does not
let one to extract proofs from the refutations. On the other hand,
direct methods (cf. \cite{far}, \cite{abadi}) are local which
gives not much practical use of them. This paper presents some
arguments on generalization of the classical propositional resolution
method to the language of modal logic. We give a resolution calculus
for modal logic $\K$ that inherits some features of classical resolution
and propose some suggestions of how can it be used for other modal logics.
No
expertsonly
published
notspecified
Y.
Kazakov
Yevgeny
W.
Charatonik
Witold
H.
Ganzinger
Harald
C1256104005ECAFCCC1565330A853629C1256D2000528115Kazakov2002
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021472010120287:932
ConferencePaper
Constraints and Theorem Proving
English
Springer
Berlin, Germany
2001
20030901
159
201
GifsurYvette, France
19990805
Contraints in Computational Logics, International Summer School (CCL99)
Lecture Notes in Computer Science
This paper is a tutorial on methods
for firstorder theorem proving with constraints.
No
expertsonly
published
notspecified
H.
Ganzinger
Harald
R.
Nieuwenhuis
Robert
H.
Comon
Hubert
C.
Marché
Claude
R.
Treinen
Ralf
3540419500
C1256104005ECAFC09CCE91D7D10F1D7C1256AB5005B7F2DGanzingerNieuwenhuis01ccl
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021562010120287:932
ConferencePaper
A Framework for Circular AssumeGuarantee Rules
English
MaxPlanckInstitut für Informatik
Saarbrücken, Germany
2002
20030811
55
58
Saarbrücken, Germany
20020304
Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi
MPI Research Report
No
expertsonly
published
notspecified
P.
Maier
Patrick
W.
Charatonik
Witold
H.
Ganzinger
Harald
C1256104005ECAFCCEB349262981FB72C1256D0A003483B3Maier2002
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021602010120287:932
Article
The undecidability of the firstorder theories of one step rewriting in linear canonical systems
English
2002
20030729
182
213
Information and Computation
175
No
expertsonly
published
joureview
S.
Vorobyov
Sergei
C1256104005ECAFC2A710DEFDA246A5AC1256AAF00436D5FVorobyov2000OSR
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021612010120287:932
ConferencePaper
On uniform word problems involving bridging operators on distributive lattices
English
Springer
Berlin, Germany
2002
20030901
235
250
Copenhagen, Denmark
20020730
Automated Reasoning with Analytic and Related Methods : International Conference, TABLEAUX 2002
Lecture Notes in Artificial Intelligence
In this paper we analyze some fragments of the universal theory
of distributive lattices with many sorted bridging operators.
Our interest in such algebras
is motivated by the fact that, in description logics,
numerical features are often expressed by using maps that
associate numerical values to sets (more generally,
to lattice elements).
We first establish a link between satisfiability
of universal sentences
with respect to algebraic models and satisfiability with respect to
certain classes of relational structures.
We use these results for giving a method for
translation to clause form of universal sentences,
and provide some decidability results based on the use of
resolution or hyperresolution.
Links between hyperresolution and tableau methods are also
discussed, and a tableau procedure for checking satisfiability
of formulae of type $t_1 \leq t_2$ is obtained by using a
hyperresolution calculus.
No
expertsonly
published
notspecified
V.
SofronieStokkermans
Viorica
U.
Egly
Uwe
C.
Fermüller
Christian
3540439293
C1256104005ECAFCF9FCEB2398137AE1C1256BBC00400F22SofronieStokkermanstableaux2002
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
Copyright Springer Verlag
oai:edoc.mpg.de:2021622010120287:932
ConferencePaper
Relative Completeness of Abstraction Refinement for Software Model Checking
English
Springer
Berlin, Germany
2002
20030901
158
172
Grenoble, France
20020408
Tools and algorithms for the construction and analysis of systems : 8th International Conference, TACAS 2002
Lecture Notes in Computer Science
No
expertsonly
published
notspecified
A.
Podelski
Andreas
T.
Ball
Tom
S.K.
Rajamani
Sriram K.
J.P.
Kaoen
JoostPieter
P.
Stevens
Perdita
3540434194
C1256104005ECAFC13C94791C65D700CC1256D09004F7FE2BPRTacas03
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021632010120287:932
ConferencePaper
An Algebraic Framework for Abstract Model Checking
English
Springer
Berlin, Germany
2002
20030901
152
169
Montreal
20020802
Abstraction, reformulation, and approximation : 5th International Symposium, SARA 2002
Lecture Notes in Computer Science
No
expertsonly
published
notspecified
S.
Mukhopadhyay
Supratik
A.
Podelski
Andreas
S.
Koenig
Sven
R.C.
Holte
Robert C.
3540439412
C1256104005ECAFCCA09461A049DB278C1256D0A00329CF4MPSARA02
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021652010120287:932
Article
Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I)
English
2002
20030729
777
829
Journal of Symbolic Computation
33
We present superposition calculi in which the axioms
of cancellative abelian monoids and, optionally, the
torsionfreeness axiom are integrated. Cancellative
abelian monoids comprise abelian groups, but also such
ubiquitous structures as the natural numbers or multisets.
Our calculi require neither extended clauses nor explicit
inferences with the theory axioms. Compared with
ACsuperposition calculi, the number of variable overlaps
is significantly reduced by strong ordering restrictions.
No
expertsonly
published
joureview
U.
Waldmann
Uwe
07477171
C1256104005ECAFC0FE819BCE345C3C0C1256CAE005B3962Waldmann2002aJSC
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021662010120287:932
ConferencePaper
A New Input Technique for Accented Letters in Alphabetical Scripts
English
The Unicode Consortium
Mountain View, CA, USA
2002
20030901
C12
Washington, DC, USA
20020128
Proceedings of the 20th International Unicode Conference
SITMO is a new input technique for accented and special
letters of the Latin alphabet (or other alphabets of comparable
size), which combines in a uniform way short key sequences for
frequently used characters with an easily memorizable scheme to
enter rarely used characters. Compared with traditional modifier
techniques, SITMO requires less additional keys and allows
to access more characters, while for most European languages,
the average number of keystrokes per derived letter is similar
(that is, close to 2).
no proper page numbers (all articles are individually numbered),
no ISBN
No
expertsonly
published
notspecified
U.
Waldmann
Uwe
C1256104005ECAFCB993844CBF744101C1256CAE0059033BWaldmann2002IUC
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021672010120287:932
Article
$\forall\exists^5$equational theory of context unification is undecidable
English
2002
20030729
463
479
Theoretical Computer Science
275
No
expertsonly
published
joureview
S.
Vorobyov
Sergei
C1256104005ECAFC918F900524C87A16C1256AAF0043B0B9Vorobyov2000aecu
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021692010120287:932
Article
An Algorithm for Isolating the Real Solutions of Semialgebraic Systems
English
2002
20030901
461
477
Journal of Symbolic Computation
34
No
expertsonly
published
joureview
B.
Xia
Bican
L.
Yang
Lu
C1256104005ECAFCBDA7B7FCC5856496C1256C7E0033236DXiaYang02
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2021702010120287:932
ConferencePaper
SPASS Version 2.0
English
Springer
Heidelberg, Germany
2002
20030901
275
279
Kopenhagen, Denmark
20020727
Automated deduction, CADE18 : 18th International Conference on Automated Deduction
Lecture Notes in Artificial Intelligence
SPASS is an automated theorem prover for full firstorder logic with equality.
This system description provides an overview of recent developments in SPASS
2.0, including among others an implementation of contextual rewriting,
refinements of the clause normal form transformation, and enhancements of the
inference engine.
No
expertsonly
published
notspecified
C.
Weidenbach
Christoph
U.
Brahm
Uwe
T.
Hillenbrand
Thomas
E.
Keen
Enno
C.
Theobalt
Christian
D.
Topić
Dalibor
A.
Voronkov
Andrei
3540439315
C1256104005ECAFCCF921E461CE82D57C1256BBB004574BFWBH+02CADE18
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312422010120287:932
ConferencePaper
Logic Programming Infrastructure for Inferences on FrameNet
English
Springer
Berlin
2004
20050202
591
603
Lisbon, Portugal
20040927
Logics in artificial intelligence : 9th European Conference, JELIA 2004
Lecture Notes in Artificial Intelligence
No
expertsonly
published
P.
Baumgartner
Peter
A.
Burchardt
Aljoscha
J.
Alferes
José
J.
Leite
João
3540232427
C1256104005ECAFC5AE12A227ED0507FC1256F8C003EEAB2Baumgartner:Burchardt:LPFrameNet:JELIA:2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312432010120287:932
ConferencePaper
Darwin: A Theorem Prover for the Model Evolution Calculus
English
UCC
Cork, Ireland
2004
20050202
1
24
Cork, Ireland
20040703
Proceedings of the 1st Workshop on Empirically Successful First Order Reasoning (ESFOR'04)
IJCAR 2004 Workshop Proceedings
No
expertsonly
published
P.
Baumgartner
Peter
A.
Fuchs
Alexander
C.
Tinelli
Cesare
S.
Schulz
Stephan
T.
Tammet
Tanel
G.
Sutcliffe
Geoff
C1256104005ECAFC885D50EF8A8E0550C1256F8C00475D39Baumgartner:etal:Darwin:ESFOR:2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312442010120287:932
ConferencePaper
Model Based Deduction for Database Schema Reasoning
English
Springer
Berlin, Germany
2004
20050427
168
182
Ulm, Germany
20040920
KI 2004: Advances in Artificial Intelligence: 27th Annual German Conference on AI, KI 2004
Lecture Notes in Artificial Intelligence
We aim to demonstrate that automated deduction techniques, in particular those
following the model computation paradigm, are very well suited for database
schema/query reasoning. Specifically, we present an approach to compute
completed paths for database or XPath queries. The database schema and a query
are transformed to disjunctive logic programs with default negation, using a
description logic as an intermediate language. Our underlying deduction system,
KRHyper, then detects if a query is satisfiable or not. In case of a
satisfiable query, all completed paths – those that fulfill all given
constraints – are returned as part of the computed models.
The purpose of computing completed paths is to reduce the workload on a query
processor. Without the path completion, a usual XPath query processor would
search the whole database for solutions to the query, which need not be the
case when using completed paths instead.
We understand this paper as a first step, that covers a basic schema/query
reasoning task by modelbased deduction. Due to the underlying expressive logic
formalism we expect our approach to easily adapt to more sophisticated problem
settings, like type hierarchies as they evolve within the XML world.
No
expertsonly
published
P.
Baumgartner
Peter
U.
Furbach
Ulrich
M.
GrossHardt
Margret
T.
Kleemann
Thomas
S.
Biundo
Susanne
T.
Frühwirth
Thom
G.
Palm
Günther
3540231668
C1256104005ECAFCFB9ED61FE483B97FC1256F8C0046D5A6Baumgartner:etal:ModelBasedSchemaReasoning:KI:2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312452010120287:932
Article
Living Book  Deduction, Slicing, and Interaction
English
2004
20050202
259
286
Journal of Automated Reasoning
32
No
expertsonly
published
joureview
P.
Baumgartner
Peter
U.
Furbach
Ulrich
M.
GrossHardt
Margret
A.
Sinner
Alex
C1256104005ECAFC22E5694CBC6673B5C1256F8C003DE880Baumgartner:EtAl:LivingBook:JAR:2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312462010120287:932
Article
In2Math  Interaktive Mathematik und Informatikgrundausbildung
German
2004
20050202
36
45
SoftwaretechnikTrends
24
No
expertsonly
published
joureview
P.
Baumgartner
Peter
B.
Grabowski
Barbara
W.
Oevel
Walter
E.
Melis
Erica
07208928
C1256104005ECAFCC26BE7D75FBB1A29C1256F8C0047CEC2Baumgartner:etal:in2math:swtechnik:2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312472010120287:932
ConferencePaper
Improving Stable Models Based Planning by Bidirectional Search
English
ALLIED
New Delhi
2004
20050202
404
413
Hyderabad, India
20041219
Proceedings of the 5th International Conference on Knowledge Based Computer Systems (KBCS 2004)
No
expertsonly
published
P.
Baumgartner
Peter
A.
Mediratta
Anupam
M.
Sasikumar
M.
R.
Vakil
R.
M.
Kavitha
M.
8177647113
C1256104005ECAFC5024C5BD02D8CB93C1256F8C003B2421Baumgartner:Mediratta:ASPPlanningBidirectional:KBCS:2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312482010120287:932
ConferencePaper
Conformant Planning via Heuristic Forward Search: A New Approach
English
AAAI
Menlo Park, USA
2004
20050202
355
364
Whistler, Canada
20040603
Proceedings of the Fourteenth International Conference on Automated Planning and Scheduling (ICAPS 2004)
No
expertsonly
published
R.
Brafman
Ronen
J.
Hoffmann
Jörg
S.
Zilberstein
Shlomo
J.
Koehler
Jana
S.
Koenig
Sven
1577352009
C1256104005ECAFCC4F81CA319526E04C1256F580046D8FBBrafmanHoffmann2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312492010120287:932
ConferencePaper
L'atelier FOCAL
French
Université de FrancheComté
Besançon, France
2004
20050609
321
324
Besançon, France
20040616
Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2004)
No
expertsonly
published
C.
Dubois
Catherine
M.
Jaume
Mathieu
O.
Pons
Olivier
V.
Prevosto
Virgile
J.
Juilland
Jacques
C1256104005ECAFCB5987F965B6F406BC1256F95005F2C80Prevosto2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312502010120287:932
ConferencePaper
DPLL(T): Fast Decision Procedures
English
Springer
Berlin, Germany
2004
20050427
175
188
Boston, Massachusetts
20040613
Computer aided verification : 16th International Conference, CAV 2004
Lecture Notes in Computer Science
No
expertsonly
published
H.
Ganzinger
Harald
G.
Hagen
George
R.
Nieuwenhuis
Robert
A.
Oliveras
Albert
C.
Tinelli
Cesare
R.
Alur
Rajeev
D.
Peled
Doron
3540223428
C1256104005ECAFC4AA28FCCECA41584C1256EBC0042AA67GanHNOTCAV04
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312512010120287:932
ConferencePaper
Integration of equational reasoning into instantiationbased theorem proving
English
Springer
Berlin
2004
20050202
71
84
Karpacz, Poland
20040920
Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL
Lecture Notes in Computer Science
In this paper we present a method for integrating equational reasoning into
instantiationbased theorem proving. The method employs a satisfiability solver
for ground equational clauses together with an instance generation process
based on an ordered paramodulation type calculus for literals. The completeness
of the procedure is proved using the the model generation technique, which
allows us to justify redundancy elimination based on appropriate orderings.
No
expertsonly
published
H.
Ganzinger
Harald
K.
Korovin
Konstantin
J.
Marcinkowski
Jerzy
A.
Tarlecki
Andrzej
3540230246
C1256104005ECAFCBF63DC0F8D07033EC1256F90005FF675GanzKor:InstEq:2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312522010120287:932
Article
Fast Term Indexing with Coded Context Trees
English
2004
20050202
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
stateoftheart 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
C1256104005ECAFCB0EF8A197F4BBBE400256D20003B728CGanzingerNieuwenhuisNivela03jar
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312532010120287:932
ConferencePaper
Modular Proof Systems for Partial Functions with Weak Equality
English
Springer
Berlin
2004
20050202
168
182
Cork, Ireland
20040704
Automated reasoning : Second International Joint Conference, IJCAR 2004
Lecture Notes in Artificial Intelligence
The paper presents a modular superposition calculus for the
combination of firstorder theories involving both total
and partial functions. Modularity means that inferences are
pure, only involving clauses over the alphabet of either
one, but not both, of the theories. The calculus is shown
to be complete provided that functions that are not in the
intersection of the component signatures are declared as
partial. This result also means that if the
unsatisfiability of a goal modulo the combined theory does
not depend on the totality of the functions in the
extensions, the inconsistency will be effectively found.
Moreover, we consider a constraint superposition calculus
for the case of hierarchical theories and show that it has
a related modularity property. Finally we identify cases
where the partial models can always be made total so that
modular superposition is also complete with respect to the
standard (total function) semantics of the theories.
No
expertsonly
published
H.
Ganzinger
Harald
V.
SofronieStokkermans
Viorica
U.
Waldmann
Uwe
D.
Basin
David
M.
Rusinowitch
Michael
3540223452
C1256104005ECAFC827C5504FD548DB8C1256EAC0033F34DGanzingerSofronieStokkermansWaldmannijcar2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312542010120287:932
ConferencePaper
SCAN is complete for all {Sahlqvist} formulae
English
Springer
Berlin, Germany
2004
20050427
149
162
Bad Malente, Germany
20030512
Relational and KleeneAlgebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra
Lecture Notes in Computer Science
SCAN is an algorithm for reducing monadic existential secondorder logic
formulae to equivalent simpler formulae, often firstorder logic
formulae. It is provably impossible for such a reduction to firstorder
logic to be always successful, even if there is an equivalent
firstorder formula for a secondorder logic formula. In this paper we
show that SCAN successfully computes the firstorder equivalents of all
Sahlqvist formulae in the classical (multi)modal language.
No
expertsonly
published
V.
Goranko
Valentin
U.
Hustadt
Ullrich
R.A.
Schmidt
Renate A.
D.
Vakarelov
Dimiter
R.
Berghammer
Rudolf
B.
Möller
Bernhard
G.
Struth
Georg
354022145X
C1256104005ECAFC655330F67680582FC1256CC3004662B4GorankoHustadtSchmidtVakarelov04a
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312552010120287:932
Article
Ordered Landmarks in Planning
English
2004
20041126
215
278
Journal of Artificial Intelligence Research
22
No
expertsonly
published
joureview
J.
Hoffmann
Jörg
J.
Porteous
Julie
L.
Sebastia
Laura
10769757
C1256104005ECAFCC0BE5DEA7E5E5897C1256F5800576F4BHoffmannEtal2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312562010120287:932
Article
Set Computation for Nonlinear Control
English
2004
20050427
1
26
Reliable Computing
10
No
expertsonly
published
joureview
L.
Jaulin
Luc
S.
Ratschan
Stefan
L.
Hardouin
Laurent
C1256104005ECAFC6A481D9A2218F3FEC1256DD50036CC5DRatschan2004a
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312572010120287:932
Proceedings
Tools and algorithms for the construction and analysis of systems : 10th International Conference, TACAS 2004 ; held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004
English
Springer
Berlin
2004
20050202
2988
Barcelona, Spain
20040329
No
expertsonly
XIV, 608
published
K.
Jensen
Kurt
A.
Podelski
Andreas
354021299
C1256104005ECAFCDE7F63676755F9DCC1256F8700450175JensenPodelski2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312582010120287:932
ConferencePaper
A Polynomial Translation from the TwoVariable Guarded Fragment with Number Restrictions to the Guarded Fragment
English
Springer
Berlin, Germany
2004
20050202
372
384
Lisbon, Portugal
20040927
Logics in artificial intelligence : 9th European Conference, JELIA 2004
Lecture Notes in Artificial Intelligence
We consider a twovariable guarded fragment with number restrictions for binary
relations and give a satisfiability preserving transformation of formulas in
this fragment to the threevariable 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
3540232427
C1256104005ECAFC3E0C7DF49217CA81C1256EE20080EDACKazakov04GF2N
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
© SpringerVerlag
oai:edoc.mpg.de:2312592010120287:932
ConferencePaper
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards
English
Springer
Berlin, Germany
2004
20050202
122
136
Cork, County Cork, Ireland
20040704
Automated reasoning : Second International Joint Conference, IJCAR 2004
Lecture Notes in Artificial Intelligence
We show how wellknown refinements of ordered resolution, in particular
redundancy elimination and ordering constraints in combination with a selection
function, can be used to obtain a decision procedure for the guarded fragment
with transitive guards. Another contribution of the paper is a special scheme
notation, that allows to describe saturation strategies and show their
correctness in a concise form.
No
expertsonly
published
Y.
Kazakov
Yevgeny
H.
de Nivelle
Hans
D.
Basin
David
M.
Rusinowitch
Michael
3540223452
C1256104005ECAFC0AC2F1C6BA0170EFC1256EA9005205E5KazNiv04ResGFTG
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
© SpringerVerlag
oai:edoc.mpg.de:2312602010120287:932
ConferencePaper
Intuitionistic LTL and a New Characterization of Safety and Liveness
English
Springer
Berlin
2004
20050202
295
309
Karpacz, Poland
20040920
Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL
Lecture Notes in Computer Science
Classical lineartime temporal logic (LTL) is capable of specifying of and
reasoning about infinite behaviors only. While this is appropriate for
specifying nonterminating reactive systems, there are situations (e.g.
assumeguarantee reasoning, runtime verification) when it is desirable to be
able to reason about finite and infinite behaviors. We propose an
interpretation of the operators of LTL on finite and infinite behaviors, which
defines an intuitionistic temporal logic (ILTL). We compare the expressive
power of LTL and ILTL. We demonstrate that ILTL is suitable for
assumeguarantee reasoning and for expressing properties that relate finite and
infinite behaviors. In particular, ILTL admits an elegant logical
characterization of safety and liveness properties.
No
expertsonly
published
P.
Maier
Patrick
J.
Marcinkowski
Jerzy
A.
Tarlecki
Andrzej
C1256104005ECAFC695F50750AE689DDC1256F8200490D7EMaier2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312612010120287:932
Article
Introduction to the Special Issue on Verification and Computational Logic
English
2004
20050112
Theory and Practice of Logic Programming (TPLP)
4
No
expertsonly
published
joureview
A.
Podelski
Andreas
14710684
C1256104005ECAFC89EE3BE1B932FBCAC1256F870073F2B4LeuschelPodelski2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312622010120287:932
ConferencePaper
Transition Invariants
English
IEEE
Los Alamitos, USA
2004
20050202
32
41
Turku, Finland
20040713
Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS 2004
No
expertsonly
published
A.
Podelski
Andreas
A.
Rybalchenko
Andrey
0769521924
C1256104005ECAFC83DBEE6FA76434F1C1256F8F00481BA8PR04:TransInv
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312632010120287:932
ConferencePaper
A Complete Method for the Synthesis of Linear Ranking Functions
English
Springer
Berlin, Germany
2004
20050617
239
251
Venice, Italy
20040111
Verification, model checking, and abstract interpretation : 5th International Conference, VMCAI 2004
Lecture Notes in Computer Science
No
expertsonly
published
A.
Podelski
Andreas
A.
Rybalchenko
Andrey
G.
Levi
Giorgio
B.
Steffen
Bernhard
3540208038
C1256104005ECAFC265D696D345781D2C1256F8F0048FA80PR04:LinearRanking
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312642010120287:932
Article
Convergent Approximate Solving of Firstorder Constraints by Approximate Quantifiers
English
2004
20050427
264
281
ACM Transactions on Computational Logic
5
No
expertsonly
published
joureview
S.
Ratschan
Stefan
C1256104005ECAFC5062986501D1D47CC1256EE00056B6D9Ratschan2004b
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312652010120287:932
ConferencePaper
Robust Pole Clustering of Parametric Uncertain Systems Using Interval Methods
English
Publ. for the International Federation of Automatic Control by Elsevier
Oxford
2004
20050203
323
328
Milano
20030707
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 Dregions in the complex plane is stated as a quantified
constraint problem
that represents bounded uncertain parameters by intervals; and an
engineeringoriented
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 nonlinear 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
0080440126
C1256104005ECAFC13B500BDBD6D466DC1256D0200300F64Ratschan2002
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312662010120287:932
ConferencePaper
Two Proof Systems for Peirce Algebras
English
Springer
Berlin, Germany
2004
20050427
238
251
Bad Malente, Germany
20030512
Relational and KleeneAlgebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra
Lecture Notes in Computer Science
This paper develops and compares two tableauxstyle proof systems for
Peirce algebras.
One is a tableau refutation proof system, the other is a proof system in
the style of RasiowaSikorski.
No
expertsonly
published
R.A.
Schmidt
Renate A.
E.
Or{\l}owska
Ewa
U.
Hustadt
Ullrich
R.
Berghammer
Rudolf
B.
Möller
Bernhard
G.
Struth
Georg
354022145X
C1256104005ECAFCCA460C864E6F307AC1256CC30045F267SchmidtOrlowskaHustadt04a
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312672010120287:932
Article
MultiAgent Dynamic Logics with Informational Test
English
2004
20050202
5
36
Annals of Mathematics and Artificial Intelligence
42
This paper investigates a family of logics for reasoning about the
dynamic activities and informational attitudes of agents,
namely the agents' beliefs and knowledge.
The logics are based
on a new formalisation and semantics
of the test operator of
propositional dynamic logic
and a representation of actions which
distinguishes abstract actions from concrete actions.
The new test operator, called informational test,
can be used to formalise the beliefs and knowledge of particular agents
as dynamic modalities.
This approach is consistent
with the formalisation
of the agents' beliefs and knowledge
as K(D)45 and S5 modalities.
Properties concerning informativeness, truthfulness and
preservation of beliefs
are proved for a derivative of the informational test operator.
It is shown that common belief and common knowledge
can be expressed in the considered logics.
This means,
the logics are more expressive
than propositional dynamic logic with
an extra modality for belief or knowledge.
The logics remain decidable and belong to 2EXPTIME.
Versions of the considered logics express natural additional properties
of beliefs or knowledge and interaction of beliefs or knowledge with
actions.
It is shown that a simulation of PDL can be constructed in one of these
extensions.
No
expertsonly
published
joureview
R.A.
Schmidt
Renate A.
D.
Tishkovsky
Dmitry
10122443
C1256104005ECAFCE49AD91EC328DED4C1256EB6005EFFDDSchmidtTishkovsky03c
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312682010120287:932
Article
Interaction between Knowledge, Action and Commitment within Agent Dynamic Logic
English
2004
20050427
381
415
Studia Logica
78
This paper considers a new class of agent dynamic logics which
provide a formal means of specifying and reasoning
about the agents' activities and informational, motivational and
practical aspects of the behaviour of the agents. We present a
Hilbertstyle deductive system for a basic agent dynamic logic and
consider a number of extensions of this logic with axiom schemata
formalising interactions between knowledge and commitment (expressing an
agent's awareness of her commitments), and interactions between
knowledge and actions (expressing no learning and persistence of
knowledge after actions). The deductive systems are proved sound and
complete with respect to a Kripkestyle semantics. Each of the
considered logics is shown to have the small model property and
therefore decidable.
No
expertsonly
published
joureview
R.A.
Schmidt
Renate A.
D.
Tishkovsky
Dmitry
U.
Hustadt
Ullrich
00393215
C1256104005ECAFC2700048EC40F2286C1256EB5005DDF89SchmidtTishkovskyHustadt04a
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312692010120287:932
ConferencePaper
Resolutionbased decision procedures for the positive theory of some finitely generated varieties of algebras
English
IEEE Computer Society
Los Alamitos, USA
2004
20050126
32
37
Toronto, Canada
20040519
Proceedings of the 34th International Symposium on MultipleValued Logic (ISMVL2004)
In this paper we give resolutionbased decision procedures for
the positive theory of certain finitelygenerated varieties of
algebras. The method is based on the existence of
representation theorems for such classes of algebras.
No
expertsonly
published
V.
SofronieStokkermans
Viorica
C1256104005ECAFCEE93B3E7EBC0FEB3C1256E32004AA7BDSofronieStokkermansismvl2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312702010120287:932
ConferencePaper
Applying Automatic Planning Systems to Airport Ground Traffic Control  A Feasibility Study
English
Springer
Berlin, Germany
2004
20050617
183
197
Ulm, Germany
20040920
KI 2004: Advances in Artificial Intelligence: 27th Annual German Conference on AI, KI 2004
Lecture Notes in Artificial Intelligence
No
expertsonly
published
S.
Trueg
Sebastian
J.
Hoffmann
Jörg
B.
Nebel
Bernhard
S.
Biundo
Susanne
T.
Frühwirth
Thom
G.
Palm
Günther
3540231668
C1256104005ECAFC8ACFA97E2FABAE7AC1256F580056F5DFTruegEtal2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2312712010120287:932
ConferencePaper
A Superposition View on NelsonOppen
English
CEUR
Aachen
2004
20050202
16
20
Cork, Ireland
20040804
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
16130073
C1256104005ECAFC8EAD4DC962EDE15BC1256EE40054344AHillenbrand2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2318872010120287:932
ConferencePaper
Two Proof Systems for Peirce Algebras
English
Springer
Berlin, Germany
2004
20050427
238
251
Bad Malente, Germany
20030512
Relational and KleeneAlgebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra
Lecture Notes in Computer Science
This paper develops and compares two tableauxstyle proof systems for
Peirce algebras.
One is a tableau refutation proof system, the other is a proof system in
the style of RasiowaSikorski.
No
expertsonly
published
notspecified
R. A.
Schmidt
Renate A.
E.
Orlowska
Ewa
U.
Hustadt
Ullrich
R.
Berghammer
Rudolf
B.
Möller
Bernhard
G.
Struth
Georg
354022145X
C1256104005ECAFCCA460C864E6F307AC1256CC30045F267SchmidtOrlowskaHustadt04a
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2318942010120287:932
ConferencePaper
Intuitionistic LTL and a New Characterization of Safety and Liveness
English
Springer
Berlin
2004
20050202
295
309
Karpacz, Poland
20040920
Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL
Lecture Notes in Computer Science
Classical lineartime temporal logic (LTL) is capable of specifying of and
reasoning about infinite behaviors only. While this is appropriate for
specifying nonterminating reactive systems, there are situations (e.g.
assumeguarantee reasoning, runtime verification) when it is desirable to be
able to reason about finite and infinite behaviors. We propose an
interpretation of the operators of LTL on finite and infinite behaviors, which
defines an intuitionistic temporal logic (ILTL). We compare the expressive
power of LTL and ILTL. We demonstrate that ILTL is suitable for
assumeguarantee reasoning and for expressing properties that relate finite and
infinite behaviors. In particular, ILTL admits an elegant logical
characterization of safety and liveness properties.
No
expertsonly
published
P.
Maier
Patrick
J.
Marcinkowski
Jerzy
A.
Tarlecki
Andrzej
C1256104005ECAFC695F50750AE689DDC1256F8200490D7EMaier2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
oai:edoc.mpg.de:2319112010120287:932
ConferencePaper
L'atelier FOCAL
French
Université de FrancheComté
Besançon, France
2004
20050609
321
324
Besançon, France
20040616
Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2004)
No
expertsonly
published
C.
Dubois
Catherine
M.
Jaume
Mathieu
O.
Pons
Olivier
V.
Prevosto
Virgile
J.
Juilland
Jacques
C1256104005ECAFCB5987F965B6F406BC1256F95005F2C80Prevosto2004
MPI für Informatik
Programming Logics Group
20101202 11:37:35.381871
ResultSet_9EtqBZSIKaC_range_100199