% BibTeX Exporter written in LotusScript by Uwe Brahm,
% Please send bug reports via email to . Thanks.
% Exported: Saturday, 15. December 2018, 07:44, Server: domino/MPII/DE
@INPROCEEDINGS{AfshordelHillenbrandWeidenbach01,
AUTHOR = {Afshordel, Bijan and Hillenbrand, Thomas and Weidenbach, Christoph},
EDITOR = {Nieuwenhuis, Robert and Voronkov, Andrei},
TITLE = {First-Order Atom Definitions Extended},
BOOKTITLE = {Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Havanna, Cuba},
PUBLISHER = {Springer},
MONTH = {December},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {2250},
YEAR = {2001},
PAGES = {309--319},
}
@INPROCEEDINGS{AlthausEtAlFrocos2009,
AUTHOR = {Althaus, Ernst and Kruglov, Evgeny and Weidenbach, Christoph},
EDITOR = {Ghilardi, Silvio and Sebastiani, Roberto},
TITLE = {Superposition Modulo Linear Arithmetic {SUP(LA)}},
BOOKTITLE = {Frontiers of Combining Systems : 7th International Symposium, FroCoS 2009},
PADDRESS = {Berlin, Germany},
ADDRESS = {Trento, Italy},
PUBLISHER = {Springer},
MONTH = {September},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {5749},
ISBN = {978-3-642-04221-8},
DOI = {10.1007/978-3-642-04222-5_5},
YEAR = {2009},
PAGES = {84--99},
}
@ARTICLE{AvenhausHillenbrandLoechner2003,
AUTHOR = {Avenhaus, J{\"u}rgen and Hillenbrand, Thomas and L{\"o}chner, Bernd},
JOURNAL = {Journal of Symbolic Computation},
TITLE = {On Using Ground Joinable Equations in Equational Theorem Proving},
ADDRESS = {Amsterdam, The Netherlands},
NUMBER = {1-2},
PUBLISHER = {Elsevier},
VOLUME = {36},
ISBN = {0747-7171},
YEAR = {2003},
PAGES = {217--233},
ABSTRACT = {When rewriting and completion techniques are used for equational
theorem proving, the axiom set is saturated with the aim to get a
rewrite system that is terminating and confluent on ground terms.
To reduce the computational effort it should (1) be powerful for
rewriting and (2) create not too many critical pairs. These problems
become especially important if some operators are associative and
commutative (\AC). We show in this paper how these two goals can be
reached to some extent by using ground joinable equations for
simplification purposes and omitting them from the generation of new
facts.
%
For the special case of \AC-operators we present a simple redundancy
criterion which is easy to implement, efficient, and effective in
practice, leading to significant speed-ups.},
}
@MASTERSTHESIS{Azmy12,
AUTHOR = {Azmy, Noran},
TITLE = {Formula Renaming with Generalizations},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
ADDRESS = {Saarbr{\"u}cken},
PUBLISHER = {Universit{\"a}t des Saarlandes},
YEAR = {2012},
}
@ARTICLE{BachmairGanzinger-94-jlc,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald},
JOURNAL = {Journal of Logic and Computation},
TITLE = {Rewrite-based equational theorem proving with selection and simplification},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
NUMBER = {3},
PUBLISHER = {Oxford University Press},
VOLUME = {4},
ISBN = {0955-792X},
YEAR = {1994},
PAGES = {217--247},
NOTE = {Revised version of Technical Report MPI-I-91-208, 1991},
ABSTRACT = {We present various refutationally complete calculi for first-order clauses with
equality that allow for arbitrary selection of negative atoms in clauses.
Refutation completeness is established via the use of well-founded orderings on
clauses for defining a Herbrand model for a consistent set of clauses. We also
formulate an abstract notion of redundancy and show that the deletion of
redundant clauses during the theorem proving process preserves refutation
completeness. It is often possible to compute the closure of nontrivial sets of
clauses under application of non-redundant inferences. The refutation of goals
for such complete sets of clauses is simpler than for arbitrary sets of
clauses, in particular one can restrict attention to proofs that have support
from the goals without compromising refutation completeness. Additional
syntactic properties allow to restrict the search space even further, as we
demonstrate for so-called quasi-Horn clauses. The results in this paper contain
as special cases or generalize many known results about Knuth-Bendix-like
completion procedures (for equations, Horn clauses, and Horn clauses over
built-in Booleans), completion of first-order clauses by clausal rewriting, and
inductive theorem proving for Horn clauses.},
}
@INPROCEEDINGS{BachmairGanzingerWaldmann-92-alp,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald and Waldmann, Uwe},
EDITOR = {Kirchner, H{\'e}l{\`e}ne and Levi, G.},
TITLE = {Theorem proving for hierarchic first-order theories},
BOOKTITLE = {Algebraic and Logic Programming},
PADDRESS = {Berlin, Germany},
ADDRESS = {?},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {632},
YEAR = {1992},
PAGES = {420--434},
NOTE = {Revised version in AAECC, vol.\ 5, number 3/4, pp.\ 193--212, 1994)},
ABSTRACT = {In this work we extend previous results on theorem proving for first-order
clauses with equality to hierarchic first-order theories. Semantically such
theories are confined to conservative extensions of the base models. It is
shown that superposition together with variable abstraction and constraint
refutation is refutationally complete for sufficiently complete theories. For
the proof we introduce a concept of approximation between theorem proving
systems, which makes it possible to reduce the problem to the known case of
(flat) first-order theories. These results allow the modular combination of a
superposition-based theorem prover with an arbitrary refutational prover for
the primitive base theory, whose axiomatic repesentation in some logic may
remain hidden.},
}
@INPROCEEDINGS{BachmairGanzingerWaldmann-93-kgs,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald and Waldmann, Uwe},
EDITOR = {Gottlob, Georg and Leitsch, Alexander and Mundici, Daniele},
TITLE = {Superposition with simplification as a decision procedure for the monadic class with equality},
BOOKTITLE = {Computational Logic and Proof Theory, Third Kurt G{\"o}del Colloquium, KGC'93},
PADDRESS = {Berlin, Germany},
ADDRESS = {Brno, Czech Republic},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {713},
YEAR = {1993},
PAGES = {83--96},
NOTE = {Revised version of Technical Report MPI-I-93-204},
ABSTRACT = {We show that superposition, a restricted form of paramodulation, can be
combined with specifically designed simplification rules such that it becomes a
decision procedure for the monadic class with equality. The completeness of the
method follows from a general notion of redundancy for clauses and
superposition inferences.},
}
@INPROCEEDINGS{BachmairGanzingerWaldmann-93-lics,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald and Waldmann, Uwe},
TITLE = {Set Constraints are the Monadic Class},
BOOKTITLE = {Eighth Annual IEEE Symposium on Logic in Computer Science},
PADDRESS = {Los Alamitos, USA},
ADDRESS = {Montreal, Canada},
PUBLISHER = {IEEE},
YEAR = {1993},
PAGES = {75--83},
ABSTRACT = {We investigate the relationship between set constraints and the monadic class
of first-order formulas and show that set constraints are essentially
equivalent to the monadic class. From this equivalence we can infer that the
satisfiability problem for set constraints is complete for NEXPTIME\@. More
precisely, we prove that this problem has a lower bound of ${\rm
NTIME}(c^{n/\log n})$. The relationship between set constraints and the monadic
class also gives us decidability and complexity results for certain practically
useful extensions of set constraints, in particular ``negative'' projections
and subterm equality tests.},
}
@ARTICLE{BachmairGanzingerWaldmann-94-aaecc,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald and Waldmann, Uwe},
JOURNAL = {Applicable Algebra in Engineering, Communication and Computing (AAECC)},
TITLE = {Refutational Theorem Proving for Hierarchic First-Order Theories},
ADDRESS = {Berlin, Germany},
NUMBER = {3/4},
PUBLISHER = {Springer},
MONTH = {April},
VOLUME = {5},
ISBN = {0938-1287},
YEAR = {1994},
PAGES = {193--212},
NOTE = {Earlier Version: Theorem Proving for Hierarchic First-Order Theories, in
Giorgio Levi and H{\'e}l{\`e}ne Kirchner, editors, {\em Algebraic and Logic
Programming, Third International Conference}, LNCS 632, pages 420--434,
Volterra, Italy, September 2--4, 1992, Springer-Verlag},
ABSTRACT = {We extend previous results on theorem proving for first-order clauses with
equality to hierarchic first-order theories. Semantically such theories are
confined to conservative extensions of the base models. It is shown that
superposition together with variable abstraction and constraint refutation is
refutationally complete for theories that are sufficiently complete with
respect to simple instances. For the proof we introduce a concept of
approximation between theorem proving systems, which makes it possible to
reduce the problem to the known case of (flat) first-order theories. These
results allow the modular combination of a superposition-based theorem prover
with an arbitrary refutational prover for the primitive base theory, whose
axiomatic representation in some logic may remain hidden. Furthermore they can
be used to eliminate existentially quantified predicate symbols from certain
second-order formulae.},
}
@MASTERSTHESIS{Bankstahl06,
AUTHOR = {Bankstahl, Jan},
TITLE = {Netflow analysis of SAP R/3 traffic in an enterprise environment},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Diploma thesis},
MONTH = {June},
YEAR = {2006},
}
@MASTERSTHESIS{Bankstahl2006,
AUTHOR = {Bankstahl, Jan},
TITLE = {Netflow analysis of {SAP R/3} traffic in an enterprise},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
MONTH = {June},
YEAR = {2006},
ABSTRACT = {Enterprise environments differ significantly from the public Internet. Workload
models of each individual application are essential for performance analysis
and troubleshooting. They are also inevitable input for network capacity
planning and network simulation. To the best of the authors knowledge, there
are only few publications, that describe the characterics of private enterprise
IP networks or and virtually no papers regarding the SAP R/3 application.
This work shows an approach to analyze application specific network traffic. It
describes, how data about network usage can be captured, filtered to a specific
application, and how the data is prepared for the analysis. It will demonstrate
these steps in an enterprise environment on user related traffic of a SAP R/3
instance.},
}
@MASTERSTHESIS{Bastuck2006,
AUTHOR = {Bastuck, Andrea},
TITLE = {{Maschinell unterst{\"u}tzte Analyse eines Sicherheitsprotokolls}},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Diploma thesis},
MONTH = {September},
YEAR = {2006},
}
@INPROCEEDINGS{BaumgartnerWaldmann2009CADE,
AUTHOR = {Baumgartner, Peter and Waldmann, Uwe},
EDITOR = {Schmidt, Renate A.},
TITLE = {Superposition and Model Evolution Combined},
BOOKTITLE = {Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction},
PADDRESS = {Berlin, Germany},
ADDRESS = {Montreal, Canada},
PUBLISHER = {Springer},
MONTH = {August},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {5663},
ISBN = {978-3-642-02958-5},
DOI = {10.1007/978-3-642-02959-2_2},
YEAR = {2009},
PAGES = {17--34},
ABSTRACT = {We present a new calculus for first-order theorem proving with equality,
ME+Sup, which generalizes both the Superposition calculus and the Model
Evolution calculus (with equality) by integrating their inference rules and
redundancy criteria in a non-trivial way. The main motivation is to combine the
advantageous features of both---rather complementary---calculi in a single
framework. For instance, Model Evolution, as a lifted version of the
propositional DPLL procedure, contributes a non-ground splitting rule that
effectively permits to split a clause into non variable disjoint subclauses. In
the paper we present the calculus in detail. Our main result is its
completeness under semantically justified redundancy criteria and
simplification rules.},
}
@ARTICLE{BaumgartnerWaldmann2011,
AUTHOR = {Baumgartner, Peter and Waldmann, Uwe},
JOURNAL = {Journal of Automated Reasoning},
TITLE = {A Combined Superposition and Model Evolution Calculus},
ADDRESS = {Dordrecht},
NUMBER = {2},
PUBLISHER = {Springer},
MONTH = {August},
VOLUME = {47},
ISBN = {0168-7433},
DOI = {10.1007/s10817-010-9214-x},
YEAR = {2011},
PAGES = {191--227},
ABSTRACT = {We present a new calculus for first-order theorem proving with equality,
ME+Sup, which generalizes both the Superposition calculus and the Model
Evolution calculus (with equality) by integrating their inference rules and
redundancy criteria in a non-trivial way. The main motivation is to combine the
advantageous features of these two rather complementary calculi in a single
framework. In particular, Model Evolution, as a lifted version of the
propositional DPLL procedure, contributes a non-ground splitting rule that
effectively permits to split a clause into \emph{non} variable disjoint
subclauses. In the paper we present the calculus in detail. Our main result is
its completeness under semantically justified redundancy criteria and
simplification rules. We also show how under certain assumptions the model
representation computed by a (finite and fair) derivation can be queried in an
effective way.},
}
@MASTERSTHESIS{Bromberger12,
AUTHOR = {Bromberger, Martin},
TITLE = {Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Bachelor thesis},
ADDRESS = {Saarbr{\"u}cken},
PUBLISHER = {Universit{\"a}t des Saarlandes},
YEAR = {2012},
}
@INPROCEEDINGS{Burel2010,
AUTHOR = {Burel, Guillaume},
EDITOR = {Dawar, Anuj and Veith, Helmut},
TITLE = {Embedding Deduction Modulo into a Prover},
BOOKTITLE = {Computer Science Logic : 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL},
ORGANIZATION = {European Association for Computer Science Logic (EACSL)},
PADDRESS = {Berlin},
ADDRESS = {Brno, Czech Republic},
PUBLISHER = {Springer},
MONTH = {August},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {6247},
ISBN = {978-3-642-15204-7},
DOI = {10.1007/978-3-642-15205-4},
YEAR = {2010},
PAGES = {155--169},
ABSTRACT = {Deduction modulo consists in presenting a theory through rewrite
rules to support automatic and interactive proof search. It induces
proof search methods based on narrowing, such as the polarized
resolution modulo. We show how to combine this method with more
traditional ordering restrictions. Interestingly, no compatibility
between the rewriting and the ordering is requested to ensure
completeness. We also show that some simplification rules, such as
strict subsumption eliminations and demodulations, preserve
completeness. For this purpose, we use a new framework based on a
proof ordering. These results show that polarized resolution modulo
can be integrated into existing provers, where these restrictions
and simplifications are present. We also discuss how this
integration can actually be done by diverting the main algorithm of
state-of-the-art provers.},
}
@ARTICLE{Burel2010a,
AUTHOR = {Burel, Guillaume},
JOURNAL = {Logical Methods in Computer Science},
TITLE = {Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo},
ADDRESS = {Braunschweig},
NUMBER = {1},
PUBLISHER = {Department of Theoretical Computer Science, Technical University of Braunschweig},
VOLUME = {7},
ISBN = {1860-5974},
DOI = {10.2168/LMCS-7 (1:3) 2011},
YEAR = {2011},
PAGES = {3:1--3:31},
NOTE = {Accepted, preparing publication},
ABSTRACT = {In deduction modulo, a theory is not represented by a set of axioms but by a
congruence on propositions modulo which the inference rules of standard
deductive systems---such as for instance natural deduction---are applied.
Therefore, the reasoning that is intrinsic of the theory does not appear in the
length of proofs. In general, the congruence is defined through a rewrite
system over terms and propositions. We define a rigorous framework to study
proof lengths in deduction modulo, where the congruence must be computed in
polynomial time. We show that even very simple rewrite systems lead to
arbitrary proof-length speed-ups in deduction modulo, compared to using axioms.
As higher-order logic can be encoded as a first-order theory in deduction
modulo, we also study how to reinterpret, thanks to deduction modulo, the
speed-ups between higher-order and first-order arithmetics that were stated by
G\"odel. We define a first-order rewrite system with a congruence decidable in
polynomial time such that proofs of higher-order arithmetic can be linearly
translated into first-order arithmetic modulo that system. We also present the
whole higher-order arithmetic as a first-order system without resorting to any
axiom, where proofs have the same length as in the axiomatic presentation. },
}
@INPROCEEDINGS{Damm-Ihlemann-Sofronie-Stokkermans2011,
AUTHOR = {Damm, Werner and Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
EDITOR = {Frazzoli, Emilio and Grosu, Radu},
TITLE = {Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata},
BOOKTITLE = {HSCC'11 : Proceedings of the 2011 ACM/SIGBED Hybrid Systems: Computation and Control},
PADDRESS = {New York, NY},
ADDRESS = {Chicago, Ill.},
PUBLISHER = {ACM},
ISBN = {978-1-4503-0629-4},
DOI = {10.1145/1967701.1967714},
YEAR = {2011},
PAGES = {73--82},
ABSTRACT = {We study linear hybrid automata with dynamics of the form
$\sum a_i x_i \leq a$ and $\sum b_i {\dot x_i} \leq b$.
We show that verification of safety properties for reasonable
classes of such systems can be reduced to invariant checking
and bounded model checking and, ultimately, to checking the
validity of certain formulae (obtained using a polynomial
reduction).
We show that the problem of checking the validity of the formulae
obtained this way is typically in NP, and identify verification
tasks which can be performed in PTIME.
These reductions can also be used for parametric systems, both
for checking safety properties given constraints on parameters,
and for deriving constraints of parameters that guarantee that
safety properties hold.},
}
@ARTICLE{Damm-Ihlemann-Sofronie-Stokkermans2011-msc,
AUTHOR = {Damm, Werner and Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
JOURNAL = {Mathematics in Computer Science},
TITLE = {{PTIME} parametric verification of safety properties for reasonable linear hybrid automata},
ADDRESS = {Basel},
NUMBER = {4},
PUBLISHER = {Birkh{\"a}user},
VOLUME = {5},
ISBN = {1661-8270},
DOI = {10.1007/s11786-011-0098-x},
YEAR = {2011},
PAGES = {469--497},
ABSTRACT = {This paper identifies an industrially relevant class of
linear hybrid automata (LHA) called reasonable LHA for
which parametric verification of convex safety properties
with exhaustive entry states can be verified in polynomial
time and time-bounded reachability can be decided
in nondeterministic polynomial time for non-parametric
verification and in exponential time for
parametric verification. Properties with exhaustive entry
states are restricted to runs originating in
a (specified) inner envelope of some mode-invariant.
Deciding whether an LHA is reasonable is
shown to be decidable in polynomial time.},
}
@TECHREPORT{Damm-Ihlemann-Sofronie-Stokkermans2011-report,
AUTHOR = {Damm, Werner and Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
EDITOR = {Bernd, Becker and Damm, Werner and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {{PTIME} parametric verification of safety properties for reasonable linear hybrid automata},
INSTITUTION = {Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)},
TYPE = {Technical Report},
ADDRESS = {Saarbr{\"u}cken},
NUMBER = {ATR 70},
MONTH = {March},
ISBN = {1860-9821},
YEAR = {2011},
PAGES = {27},
ABSTRACT = {This paper identifies an industrially relevant class of
linear hybrid automata (LHA) called reasonable LHA for
which parametric verification of convex safety properties
with exhaustive entry states can be verified in polynomial
time and time-bounded reachability can be decided
in nondeterministic polynomial time for non-parametric
verification and in exponential time for
parametric verification. Properties with exhaustive entry
states are restricted to runs originating in
a (specified) inner envelope of some mode-invariant.
Deciding whether an LHA is reasonable is
shown to be decidable in polynomial time.},
}
@ARTICLE{DammDierksDischEtAl2011,
AUTHOR = {Damm, Werner and Dierks, Henning and Disch, Stefan and Hagemann, Willem and Pigorsch, Florian and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
JOURNAL = {Science of Computer Programming},
TITLE = {Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces},
ADDRESS = {Amsterdam},
PUBLISHER = {Elsevier},
VOLUME = {in press},
ISBN = {0167-6423},
DOI = {10.1016/j.scico.2011.07.006},
YEAR = {2011},
PAGES = {1--29},
}
@ARTICLE{DammDierksDischEtAl2012,
AUTHOR = {Damm, Werner and Dierks, Henning and Disch, Stefan and Hagemann, Willem and Pigorsch, Florian and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
JOURNAL = {Science of Computer Programming},
TITLE = {Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces},
ADDRESS = {Amsterdam},
NUMBER = {10-11},
PUBLISHER = {Elsevier},
MONTH = {September},
VOLUME = {77},
ISBN = {0167-6423},
DOI = {10.1016/j.scico.2011.07.006},
YEAR = {2012},
PAGES = {1122--1150},
ABSTRACT = {We propose an improved symbolic algorithm for the
verification of linear hybrid automata with large
discrete state spaces (where an explicit
representation of discrete states is difficult).
Here both the discrete part and the continuous
part of the hybrid state space are represented by
one symbolic representation called LinAIGs.
LinAIGs represent (possibly non-convex) polyhedra
extended by Boolean variables. Key components of
our method for state space traversal are
redundancy elimination and constraint
minimization: redundancy elimination eliminates
so-called redundant linear constraints from LinAIG
representations by a suitable exploitation of the
capabilities of SMT (Satisfiability Modulo
Theories) solvers. Constraint minimization
optimizes polyhedra by exploiting the fact that
states already reached in previous steps can be
interpreted as "don't cares" in the current step.
Experimental results (including comparisons to the
state-of-the-art model checkers PHAVer and RED)
demonstrate the advantages of our approach.},
}
@TECHREPORT{DammDierksHagemannEtAl2011,
AUTHOR = {Damm, Werner and Disch, Stefan and Hagemann, Willem and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
EDITOR = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas},
TITLE = {Integrating incremental flow pipes into a symbolic model checker for hybrid systems},
INSTITUTION = {Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)},
TYPE = {Technical Report},
ADDRESS = {Saarbr{\"u}cken},
NUMBER = {ATR 76},
MONTH = {July},
ISBN = {1860-9821},
YEAR = {2011},
PAGES = {14},
ABSTRACT = {We describe an approach to integrate incremental ﬂow pipe computation into a
fully symbolic backward model checker for hybrid systems. Our method combines
the advantages of symbolic state set representation, such as the ability to
deal with large numbers of boolean variables, with an effcient way to handle
continuous ﬂows deﬁned by linear differential equations, possibly including
bounded disturbances.},
}
@INPROCEEDINGS{DammDischHungarJacobsPangPigorschSchollWaldmannWirtz2007,
AUTHOR = {Damm, Werner and Disch, Stefan and Hungar, Hardi and Jacobs, Swen and Pang, Jun and Pigorsch, Florian and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
EDITOR = {Namjoshi, Kedar S. and Yoneda, Tomohiro and Higashino, Teruo and Okamura, Yoshio},
TITLE = {Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space},
BOOKTITLE = {Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007},
PADDRESS = {Berlin, Germany},
ADDRESS = {Tokyo, Japan},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4762},
ISBN = {3-540-75595-1},
DOI = {10.1007/978-3-540-75596-8_30},
YEAR = {2007},
PAGES = {425--440},
ABSTRACT = {We propose algorithms significantly extending the limits for
maintaining exact representations in the verification of linear
hybrid systems with large discrete state spaces. We use
AND-Inverter Graphs (AIGs) extended with linear constraints
(LinAIGs) as symbolic representation of the hybrid state space,
and show how methods for maintaining compactness of AIGs can be
lifted to support model-checking of linear hybrid systems with
large discrete state spaces. This builds on a novel approach for
eliminating sets of redundant constraints in such rich hybrid
state representations by a suitable exploitation of the
capabilities of SMT solvers, which is of independent value beyond
the application context studied in this paper. We used a
benchmark derived from an Airbus flap control system (containing
$2^{20}$ discrete states) to demonstrate the relevance of the
approach.},
}
@INPROCEEDINGS{DammDischHungarPangPigorschSchollWaldmannWirtz2006,
AUTHOR = {Damm, Werner and Disch, Stefan and Hungar, Hardi and Pang, Jun and Pigorsch, Florian and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
EDITOR = {Graf, Susanne and Zhang, Wenhui},
TITLE = {Automatic Verification of Hybrid Systems with Large Discrete State Space},
BOOKTITLE = {Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006},
PADDRESS = {Berlin, Germany},
ADDRESS = {Beijing, China},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4218},
ISBN = {3-540-47237-1},
YEAR = {2006},
PAGES = {276--291},
ABSTRACT = {We address the problem of model checking hybrid systems which
exhibit nontrivial discrete behavior and thus cannot be
treated by considering the discrete states one by one, as most
currently available verification tools do. Our procedure
relies on a deep integration of several techniques and tools.
An extension of AND-Inverter-Graphs (AIGs) with first-order
constraints serves as a compact representation format for sets
of configurations which are composed of continuous regions and
discrete states. Boolean reasoning on the AIGs is complemented
by firstorder reasoning in various forms and on various
levels. These include implication checks for simple
constraints, test vector generation for fast inequality checks
of boolean combinations of constraints, and an exact
subsumption check for representations of two
configurations.\par
These techniques are integrated within a model checker for
universal CTL. Technically, it deals with discrete-time hybrid
systems with linear differentials. The paper presents the
approach, its prototype implementation, and first experimental
data.},
}
@INPROCEEDINGS{Dhungana2013,
AUTHOR = {Dhungana, Deepak and Tang, Ching Hoo and Weidenbach, Christoph and Wischnewski, Patrick},
EDITOR = {Denney, Ewen and Bultan, Tevfik and Zeller, Andreas},
TITLE = {Automated Verification of Interactive Rule-Based Configuration Systems},
BOOKTITLE = {2013 28th IEEE/ACM International Conference on Automated Software Engineering},
ORGANIZATION = {Institute of Electrical and Electronics Engineers (IEEE) / Association for Computing Machinery (ACM)},
PADDRESS = {New York},
ADDRESS = {Palo Alto, USA},
PUBLISHER = {IEEE},
MONTH = {November},
ISBN = {978-1-4799-0215-6},
DOI = {10.1109/ASE.2013.6693112},
YEAR = {2013},
PAGES = {551--561},
ABSTRACT = {Rule-based specifications of systems have again
become common in the context of product line variability modeling and
configuration systems. In this paper, we define a logical
foundation for rule-based specifications that has enough expressivity
and operational behavior to be
practically useful and at the same time enables decidability of
important overall properties such as consistency or cycle-freeness.
Our logic supports rule-based interactive user transitions as well as
the definition of a domain theory via rule transitions.
As a running example, we model DOPLER, a rule-based configuration system
currently in use at Siemens.},
}
@MASTERSTHESIS{Dimova09,
AUTHOR = {Dimova, Dilyana},
TITLE = {On the Translation of Timed Automata into First-order Logic},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
ADDRESS = {Saarbr{\"u}cken},
PUBLISHER = {Universit{\"a}t des Saarlandes},
MONTH = {March},
YEAR = {2009},
}
@MASTERSTHESIS{Dimova2007,
AUTHOR = {Dimova, Dilyana},
TITLE = {Propositional Abduction},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Bachelor thesis},
MONTH = {September},
YEAR = {2007},
ABSTRACT = {Reasoning can be defined as the process of applying existing
knowledge in order to produce new knowledge. In logic, there are at least two
fundamentally different sorts of reasoning: the deductive and the abductive.
Deductive reasoning (or simply deduction) is the process of deriving
consequences from what is known or assumed to be true. On the other
hand, abductive reasoning (or simply abduction) infers what needs to be assumed
to derive a given consequence. Thus, deduction
and abduction differ in the direction in which a rule has been used
for inference.
In this work, we present a calculus to generate abductive
explanations for propositional theories. The formalism is based on
propositional resolution with Set-Of-Support strategy. Furthermore,
we investigate an extension of this calculus dealing with orderings.
},
}
@MASTERSTHESIS{Dressler09,
AUTHOR = {Dre{\ss}ler, Christian},
TITLE = {Automatic Analysis of Tree-Based Feature Models with {SPASS}},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
ADDRESS = {Saarbr{\"u}cken},
PUBLISHER = {Universit{\"a}t des Saarlandes},
MONTH = {April},
YEAR = {2009},
}
@MASTERSTHESIS{Dressler2007,
AUTHOR = {Dressler, Christian},
TITLE = {First-Order Proof Documentation},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Bachelor thesis},
MONTH = {December},
YEAR = {2007},
}
@INPROCEEDINGS{ErramiEiswirth:13a,
AUTHOR = {Errami, H. and Eiswirth, M. and Grigoriev. D. and Seiler, W. and Sturm, T. and Weber, A.},
TITLE = {Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates},
BOOKTITLE = {Proceedings of the CASC 2013},
PADDRESS = {Switzerland},
ADDRESS = {Berlin},
PUBLISHER = {Springer},
SERIES = {LNCS},
VOLUME = {8136},
YEAR = {2013},
PAGES = {88--99},
}
@MASTERSTHESIS{Esquivel13,
AUTHOR = {Esquivel Pinto, Claudia Sofia},
TITLE = {Computing Variable Orders for SAT-Problems},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
MONTH = {April},
YEAR = {2013},
}
@TECHREPORT{faber-ihlemann-jacobs-sofronie-2010-report,
AUTHOR = {Faber, Johannes and Ihlemann, Carsten and Jacobs, Swen and Sofronie-Stokkermans, Viorica},
EDITOR = {Bernd, Becker and Damm, Werner and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {Automatic Verification of Parametric Specifications with Complex Topologies},
INSTITUTION = {Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)},
TYPE = {Technical Report},
ADDRESS = {Saarbr{\"u}cken},
NUMBER = {ATR 66},
MONTH = {October},
ISBN = {1860-9821},
YEAR = {2010},
PAGES = {40},
ABSTRACT = {The focus of this paper is on reducing the complexity in
verification by exploiting modularity at various levels:
in specification, in verification, and structurally.
\begin{itemize}
\item For specifications, we use the modular language CSP-OZ-DC,
which allows us to decouple verification tasks concerning
data from those concerning durations.
\item At the verification level, we exploit modularity in
theorem proving for rich data structures and use this for
invariant checking.
\item At the structural level, we analyze possibilities
for modular verification of systems consisting of various
components which interact.
\end{itemize}
We illustrate these ideas by automatically verifying safety
properties of a case study from the European Train Control
System standard, which extends previous examples by comprising a
complex track topology with lists of track segments and trains
with different routes.},
}
@INPROCEEDINGS{faber-ihlemann-jacobs-sofronieStokkermans-ifm-2010,
AUTHOR = {Faber, Johannes and Ihlemann, Carsten and Jacobs, Swen and Sofronie-Stokkermans, Viorica},
EDITOR = {Mery, Dominique and Merz, Stephan},
TITLE = {Automatic Verification of Parametric Specifications with Complex Topologies},
BOOKTITLE = {Integrated Formal Methods : 8th International Conference, IFM 2010},
PADDRESS = {Berlin},
ADDRESS = {Nancy, France},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {6396},
ISBN = {978-3-642-16264-0},
DOI = {10.1007/978-3-642-16265-7_12},
YEAR = {2010},
PAGES = {152--167},
ABSTRACT = {The focus of this paper is on reducing the complexity in
verification by exploiting modularity at various levels:
in specification, in verification, and structurally.
\begin{itemize}
\item For specifications, we use the modular language CSP-OZ-DC,
which allows us to decouple verification tasks concerning
data from those concerning durations.
\item At the verification level, we exploit modularity in
theorem proving for rich data structures and use this for
invariant checking.
\item At the structural level, we analyze possibilities
for modular verification of systems consisting of various
components which interact.
\end{itemize}
We illustrate these ideas by automatically verifying safety
properties of a case study from the European Train Control
System standard, which extends previous examples by comprising a
complex track topology with lists of track segments and trains
with different routes.},
}
@INPROCEEDINGS{faber-jacobs-sofronie-ifm-2007,
AUTHOR = {Faber, Johannes and Jacobs, Swen and Sofronie-Stokkermans, Viorica},
EDITOR = {Davies, Jim and Gibbons, Jeremy},
TITLE = {Verifying {CSP-OZ-DC} specifications with complex data types and timing parameters},
BOOKTITLE = {Proceedings of IFM 2007: Integrated Formal Methods},
PADDRESS = {New York},
ADDRESS = {Oxford, UK},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4591},
ISBN = {978-3-540-73209-9},
DOI = {10.1007/978-3-540-73210-5_13},
YEAR = {2007},
PAGES = {233--252},
}
@INPROCEEDINGS{Fehreretal94a,
AUTHOR = {Fehrer, Detlef and Hustadt, Ullrich and Jaeger, Manfred and Nonnengart, Andreas and Ohlbach, Hans J{\"u}rgen and Schmidt, Renate A. and Weidenbach, Christoph and Weydert, Emil},
EDITOR = {Baader, Franz and Lenzerini, Maurizio and Nutt, Werner and Patel-Schneider, Peter F.},
TITLE = {Description Logics for Natural Language Processing},
BOOKTITLE = {International Workshop on Description Logics '94},
PADDRESS = {Saarbr{\"u}cken, Germany},
ADDRESS = {Bonn, Germany},
PUBLISHER = {DFKI},
SERIES = {Document},
VOLUME = {D-94-10},
YEAR = {1994},
PAGES = {80--84},
ABSTRACT = {In this paper we focus on the application of description logics to natural
language processing. In cooperation with the {\sc pracma} project we have been
developing a suitably extended knowledge representation system, called {\sc
motel}. In our approach to agent modelling and natural language processing we
use an extension of the well-known description language $\cal ALC$. Our system
{\sc motel}\ serves on one hand as a knowledge base for the natural language
front-end, and on the other hand, it provides powerful {\em logical\/}
representation and reasoning components. As our approach is logic based we hope
that this enhances the overall capabilities of the natural language processing
(NLP) system. We present a brief overview of {\sc motel} and the different
extensions we are working on, i.e.\ modal extension of description logics, a
cardinality-based approach to quantitative information, reason maintenance,
probablistic, non-monotonic, and abductive reasoning.},
}
@MASTERSTHESIS{Fietzke2007,
AUTHOR = {Fietzke, Arnaud},
TITLE = {Labelled Splitting},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
MONTH = {October},
YEAR = {2007},
ABSTRACT = {Saturation-based theorem provers are typically based on a calculus
consisting of inference and reduction rules that operate on sets of
clauses. While inference rules produce new clauses, reduction rules
allow the removal or simplification of redundant clauses and are an
essential ingredient for efficient implementations.
The power of reduction rules can be further amplified by the use of
the splitting rule, which is based on explicit case analysis on variable-
disjoint components of a clause.
In this thesis, I give a formalization of splitting and backtracking for
first-order logic using a labelling scheme that annotates clauses and
clause sets with additional information, and I present soundness and
completeness results for the corresponding calculus.
The backtracking process as formalized here generalizes optimizations
that are currently being used, and I present the results of integrating
the improved backtracking into SPASS.},
}
@INPROCEEDINGS{FietzkeKruglovWeidenbach2012,
AUTHOR = {Fietzke, Arnaud and Kruglov, Evgeny and Weidenbach, Christoph},
EDITOR = {Bj{\o}rner, Nikolaj and Voronkov, Andrei},
TITLE = {Automatic Generation of Invariants for Circular Derivations in {SUP(LA)}},
BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18},
PADDRESS = {Berlin},
ADDRESS = {M{\'e}rida, Venezuela},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7180},
ISBN = {978-3-642-28716-9},
DOI = {10.1007/978-3-642-28717-6_17},
YEAR = {2012},
PAGES = {197--211},
ABSTRACT = {The hierarchic combination of linear arithmetic and firstorder
logic with free function symbols, FOL(LA), results in a strictly
more expressive logic than its two parts. The SUP(LA) calculus can be
turned into a decision procedure for interesting fragments of FOL(LA).
For example, reachability problems for timed automata can be decided
by SUP(LA) using an appropriate translation into FOL(LA). In this paper,
we extend the SUP(LA) calculus with an additional inference rule,
automatically generating inductive invariants from partial SUP(LA)
derivations. The rule enables decidability of more expressive fragments,
including reachability for timed automata with unbounded integer variables.
We have implemented the rule in the SPASS(LA) theorem prover
with promising results, showing that it can considerably speed up proof
search and enable termination of saturation for practically relevant
problems.},
}
@ARTICLE{FietzkeWeidenbach09,
AUTHOR = {Fietzke, Arnaud and Weidenbach, Christoph},
JOURNAL = {Annals of Mathematics and Artificial Intelligence},
TITLE = {Labelled Splitting},
ADDRESS = {New York, NY},
NUMBER = {1-2},
PUBLISHER = {Springer},
MONTH = {July},
VOLUME = {55},
ISBN = {1012-2443},
DOI = {10.1007/s10472-009-9150-9},
YEAR = {2009},
PAGES = {3--34},
}
@TECHREPORT{FietzkeWeidenbach2008,
AUTHOR = {Fietzke, Arnaud and Weidenbach, Christoph},
TITLE = {Labelled Splitting},
INSTITUTION = {MPI-INF RG1},
TYPE = {Research Report},
ADDRESS = {MPI f{\"u}r Informatik, Campus E 1 4, 66123 Saarbr{\"u}cken},
NUMBER = {MPI-I-2008-RG1-001},
MONTH = {September},
YEAR = {2008},
PAGES = {45},
ABSTRACT = {We define a superposition calculus with explicit splitting and
an explicit, new backtracking rule on the basis of labelled clauses.
For the first time we show a superposition calculus with explicit
backtracking rule sound and complete. The new backtracking rule advances
backtracking with branch condensing known from SPASS.
An experimental evaluation of an implementation of the new rule
shows that it improves considerably the
previous SPASS splitting implementation.
Finally, we discuss the relationship between labelled first-order
splitting and DPLL style splitting with intelligent backtracking
and clause learning.},
}
@INPROCEEDINGS{FietzkeWeidenbach2010,
AUTHOR = {Fietzke, Arnaud and Hermanns, Holger and Weidenbach, Christoph},
EDITOR = {Ferm{\"u}ller, Christian G. and Voronkov, Andrei},
TITLE = {Superposition-based Analysis of First-Order Probabilistic Timed Automata},
BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning : 17th International Conference, LPAR-17},
PADDRESS = {Berlin},
ADDRESS = {Yogyakarta, Indonesia},
PUBLISHER = {Springer},
MONTH = {October},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {6397},
ISBN = {978-3-642-16241-1},
DOI = {10.1007/978-3-642-16242-8},
YEAR = {2010},
PAGES = {302--316},
ABSTRACT = {This paper discusses the analysis of first-order probabilistic
timed automata (FPTA) by a combination of hierarchic first-order
superposition-based theorem proving and probabilistic model checking.
We develop the overall semantics of FPTAs and prove soundness and
completeness of our method for reachability properties. Basically, we decompose
FPTAs into their time plus first-order logic aspects on the one
hand, and their probabilistic aspects on the other hand. Then we exploit
the time plus first-order behavior by hierarchic superposition over
linear arithmetic. The result of this analysis is the basis for the construction
of a reachability equivalent (to the original FPTA) probabilistic
timed automaton to which probabilistic model checking is finally applied.
The hierarchic superposition calculus required for the analysis is
sound and complete on the first-order formulas generated from FPTAs.
It even works well in practice. We illustrate the potential behind it with
a real-life DHCP protocol example, which we analyze by means of tool
chain support.},
}
@INPROCEEDINGS{FietzkeWeidenbach2011,
AUTHOR = {Fietzke, Arnaud and Weidenbach, Christoph},
EDITOR = {Ratschan, Stefan},
TITLE = {Superposition as a Decision Procedure for Timed Automata},
BOOKTITLE = {Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2011)},
PADDRESS = {Beijing, China},
ADDRESS = {Beijing, China},
PUBLISHER = {Internal Conference Proceedings},
YEAR = {2011},
ABSTRACT = {The success of superposition-based theorem proving in
first-order logic relies in particular on the fact that
the superposition calculus is able to decide well-known
classical decidable fragments of first-order logic and
has been successful in identifying new decidable classes.
In this paper, we extend this story to the hierarchic combination
of linear arithmetic and first-order superposition. We show
that decidability of reachability in timed automata can
be obtained by instantiation of an abstract termination result for SUP(LA),
the hierarchic
combination of linear arithmetic and first-order superposition.},
}
@INPROCEEDINGS{FietzkeWeidenbachCADE08,
AUTHOR = {Fietzke, Arnaud and Weidenbach, Christoph},
TITLE = {Labelled Splitting},
BOOKTITLE = {IJCAR},
PADDRESS = {Berlin/Heidelberg},
ADDRESS = {Sydney, Australia},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {5195},
ISBN = {978-3-540-71069-1},
YEAR = {2008},
PAGES = {459--474},
}
@ARTICLE{FietzkeWeidenbachMCS2012,
AUTHOR = {Fietzke, Arnaud and Weidenbach, Christoph},
JOURNAL = {Mathematics in Computer Science},
TITLE = {Superposition as a Decision Procedure for Timed Automata},
ADDRESS = {Basel},
NUMBER = {4},
PUBLISHER = {Birkh{\"a}user},
MONTH = {December},
VOLUME = {6},
ISBN = {1661-8289},
DOI = {10.1007/s11786-012-0134-5},
YEAR = {2012},
PAGES = {409--425},
ABSTRACT = {The success of superposition-based theorem proving in first-order logic relies
in particular on the fact that the superposition calculus can be turned into a
decision procedure for various decidable fragments of first-order logic and has
been successfully used to identify new decidable classes. In this paper, we
extend this story to the hierarchic combination of linear arithmetic and
first-order superposition. We show that decidability of reachability in timed
automata can be obtained by instantiation of an abstract termination result for
SUP(LA), the hierarchic combination of linear arithmetic and first-order
superposition.},
}
@INPROCEEDINGS{FontaineMerzWeidenbach12,
AUTHOR = {Fontaine, Pascal and Merz, Stephan and Weidenbach, Christoph},
TITLE = {Combination of Disjoint Theories: Beyond Decidability},
BOOKTITLE = {Proceedings of the 6th International Joint Conference on Automated Reasoning},
PADDRESS = {Berlin Heidelberg},
ADDRESS = {Manchester, UK},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7364},
YEAR = {2012},
}
@ARTICLE{Freiheit2005,
AUTHOR = {Freiheit, J{\"o}rn and Luuk, Marc and M{\"u}nch, Susanne and Sijanski, Grozdana and Zangl, Fabrice},
JOURNAL = {Digital Evidence Journal},
TITLE = {Lexecute: Visualisation and representation of legal procedures},
ADDRESS = {Bedfordshire, UK},
NUMBER = {1},
PUBLISHER = {Pario Communications Limited},
MONTH = {May},
VOLUME = {3},
ISBN = {1750-7200},
YEAR = {2006},
PAGES = {17--27},
}
@INPROCEEDINGS{Freiheit2005b,
AUTHOR = {Freiheit, J{\"o}rn and Zangl, Fabrice},
EDITOR = {Remenyi, Dan},
TITLE = {Model-based user-interface management for public services},
BOOKTITLE = {6th European Conference on e-Government},
PADDRESS = {Reading, UK},
ADDRESS = {Marburg, Germany},
PUBLISHER = {Academic Conferences Limited},
MONTH = {April},
ISBN = {1-905305-19-2cd},
YEAR = {2006},
PAGES = {141--151},
}
@INPROCEEDINGS{Freiheit2005c,
AUTHOR = {Lilith, Nimrod and Billington, Jonathan and Freiheit, J{\"o}rn},
EDITOR = {Lenzini, Luciano and Cruz, Rene L.},
TITLE = {Approximate Closed-Form Aggregation of a Fork-Join Structure in Generalised Stochastic Petri Nets},
BOOKTITLE = {Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, VALUETOOLS 2006},
PADDRESS = {New York, USA},
ADDRESS = {Pisa, Italy},
PUBLISHER = {ACM},
SERIES = {ACM International Conference Proceeding Series},
VOLUME = {180},
ISBN = {1-59593-504-5},
YEAR = {2006},
PAGES = {1--10},
ABSTRACT = {In this paper an aggregation technique for generalised stochastic Petri nets
(GSPNs) possessing synchronised parallel structures is presented. Parallel
processes featuring synchronisation constraints commonly occur in fields such
as product assembly and computer process communications, however their
existence in closed networks severely complicates analysis. This paper details
the derivation of computationally-simple closed-form expressions which permit
the aggregation of a GSPN subnet featuring a fork-join structure. The
aggregation expressions presented in this paper do not require the generation
of the underlying continuous time Markov chain of the original net, and do not
follow an iterative procedure. The resulting aggregated GSPN accurately
approximates the stationary token distribution behaviour of the original net,
and this is shown by the analysis of a number of example GSPNs.},
}
@INPROCEEDINGS{Freiheit2005d,
AUTHOR = {Simon, Carlo and Freiheit, J{\"o}rn and Olbrich, Sebastian},
EDITOR = {N{\"u}ttgens, Markus and Rump, Frank J. and Mendling, Jan},
TITLE = {Using BPEL processes defined by Event-driven Process Chains},
BOOKTITLE = {5. GI-Workshop "EPK 2006 - Gesch{\"a}ftsprozessmanagement mit Ereignisgesteuerten Prozessketten"},
PADDRESS = {Aachen, Germany},
ADDRESS = {Vienna, Austria},
PUBLISHER = {CEUR Workshop Proceedings},
YEAR = {2006},
PAGES = {121--135},
}
@ARTICLE{Freiheit2007a,
AUTHOR = {Freiheit, J{\"o}rn and Zangl, Fabrice},
JOURNAL = {Electronic Journal of e-Government},
TITLE = {Model-based User-interface Management for Public Services},
ADDRESS = {Kidmore End, UK},
NUMBER = {1},
PUBLISHER = {Academic Conferences Limited},
MONTH = {June},
VOLUME = {5},
ISBN = {1479-439X},
YEAR = {2007},
PAGES = {53--62},
ABSTRACT = {Public business processes can be very complex. That makes it hard for citizens
to understand these processes and for software companies to implement them into
software tools. Changes of the process entail expensive effort in both teaching
the citizens and adapting the software. For business processes several
model-based approaches have been suggested to deal with high complexity, such
as BPMN. However, modelling simplifies work of software developers rather than
of citizens. We present an approach where an adequate user-interface with
user-centric pertinent information is derived directly from the models. Our
approach combines the advantages of having models for the software developers
with the requirements of the users.
The modelling technique we are using is Event-driven Process Chains (EPCs).
EPCs are widely accepted in the commercial area and are comprehensively
investigated in the academic area as well. Due to their graphical description
they are easy to understand. EPCs are implemented in the ARIS toolset, which
offers the possibility to attach attributes to the elements of the EPCs. This
paper will demonstrate how these attributes are used to derive a
user-interface, e.g. a relevant website or document, for each state or
transition of the EPC. The tools used extract the values of the attributes and
incorporate them into a web-based user-interface according to the EPC of the
modelled business process. Execution of the model then is equivalent to running
the user-interface. A change of the process requires a change of the model
only, which is much easier to handle than changing the implementation of the
user-interface.},
}
@ARTICLE{Freiheit2007c,
AUTHOR = {Ziemann, Joerg and Matheis, Thomas and Freiheit, J{\"o}rn},
JOURNAL = {Enterprise Modelling and Information Systems Architectures},
TITLE = {Modelling of Cross-Organizational Business Processes - Current Methods and Standards},
NUMBER = {2},
PUBLISHER = {German Informatics Society},
MONTH = {November},
VOLUME = {2},
YEAR = {2007},
PAGES = {23--31},
ABSTRACT = {Not only since the upcoming of Service-oriented Architectures the modelling of
cross-organizational business processes is a heavily investigated field
comprising dozens of standards based on different concepts. New techniques on
the implementation site, e.g. Web Service orchestration and choreography,
further extended the possibilities and requirements on such standards. To
systematically order and present a comprehensive state of the art of relevant
methods and standards this paper first describes requirements that occur in
cross-organizational business processes both for concepts and modelling
languages. Then the most important state of the art concepts for modelling
cross-organizational processes are described. Based on the requirements defined
before and the presented concepts, selected modelling languages are analysed.},
}
@INPROCEEDINGS{Freiheit2007d,
AUTHOR = {Ziemann, Joerg and Matheis, Thomas and Freiheit, J{\"o}rn},
TITLE = {Modelling of Cross-Organizational Business Processes},
BOOKTITLE = {Enterprise Modelling and Information Systems Architectures 2007},
ORGANIZATION = {German Informatics Society SIG MoBIS},
PADDRESS = {Bonn},
ADDRESS = {St. Goar, Germany},
PUBLISHER = {SIG MoBIS},
MONTH = {October},
YEAR = {2007},
PAGES = {87--95},
}
@PROCEEDINGS{ftp09,
EDITOR = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
TITLE = {First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving, Proceedings},
PADDRESS = {Oslo, Norway},
ADDRESS = {Oslo, Norway},
PUBLISHER = {University of Oslo/Department of Informatics},
MONTH = {June},
SERIES = {University Oslo/Department of Informatics: Research Report},
VOLUME = {386},
ISBN = {82-7368-347-8},
YEAR = {2009},
PAGES = {151},
}
@INPROCEEDINGS{GaillourdetHillenbrandLoechner2003,
AUTHOR = {Gaillourdet, Jean-Marie and Hillenbrand, Thomas and L{\"o}chner, Bernd and Spies, Hendrik},
EDITOR = {Baader, Franz},
TITLE = {The New {WALDMEISTER} Loop at Work},
BOOKTITLE = {Automated deduction, CADE-19 : 19th International Conference on Automated Deduction},
PADDRESS = {Berlin, Germany},
ADDRESS = {Miami, Florida},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {2741},
YEAR = {2003},
PAGES = {317--321},
ABSTRACT = {We present recent developments within the theorem prover \textsc{Waldmeister}.
They rely on a novel organization of the underlying saturation-based proof
procedure into a system architecture. As is known, the saturation process tends
to quickly fill the memory available unless preventive measures are employed.
To overcome this problem, our new ``\textsc{Waldmeister} loop'' features a
highly compact representation of the search state, exploiting its inherent
structure. The implementation just being available, the cost and the benefits
of the concept now can exactly be measured. Indeed are our expectations met
concerning the drastic cut-down of memory usage with only moderate overhead of
time.
In addition it has turned out that the revealed structure of the search state
paves the way to an easily implemented parallelization of the prover with
modest communication requirements and rewarding speed-ups. In order to minimize
communication-related latencies, we discuss some variations of the loop to
maximally profit from multiple processors.},
}
@INPROCEEDINGS{GanKor:ThInst:2006,
AUTHOR = {Ganzinger, Harald and Korovin, Konstantin},
EDITOR = {Hermann, Miki and Voronkov, Andrei},
TITLE = {Theory Instantiation},
BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference (LPAR'06)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Phnom Penh, Cambodia},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4246},
ISBN = {3-540-4828-4},
YEAR = {2006},
PAGES = {497--511},
ABSTRACT = {In this paper we present a method of integrating theory
reasoning into the instantiation framework. One of the distinctive features of
our approach is that it allows
us to employ off-the-shelf satisfiability solvers for ground
clauses modulo theories, as a part of general first-order
reasoning. As an application of this approach, we show how
it is possible to combine the instantiation calculus with
other calculi, such as ordered resolution and paramodulation.},
}
@UNPUBLISHED{Ganzinger-94-sat,
AUTHOR = {Ganzinger, Harald},
TITLE = {The {Saturate} System},
YEAR = {1994},
NOTE = {Available on the World-Wide Web and URL
http://www.mpi-sb.mpg.de/SATURATE/Saturate.html},
ABSTRACT = {The Saturate system is an experimental theorem prover based on saturation. It
has originally been developed as an implementation of the superposition
calculus by Pilar Nivela and Robert Nieuwenhuis from the Technical University
of Catalonia, Barcelona. The version the use of which is described in this
document now contains extensions by chaining techniques for arbitrary
transitive relations implemented by Harald Ganzinger, MPI Informatik,
Saarbr\"ucken, with the help of Robert Nieuwenhuis.},
}
@INPROCEEDINGS{Ganzinger-SofronieStokkermans-Waldmann-ijcar-2004,
AUTHOR = {Ganzinger, Harald and Sofronie-Stokkermans, Viorica and Waldmann, Uwe},
EDITOR = {Basin, David and Rusinowitch, Michael},
TITLE = {Modular Proof Systems for Partial Functions with Weak Equality},
BOOKTITLE = {Automated reasoning : Second International Joint Conference, IJCAR 2004},
PADDRESS = {Berlin},
ADDRESS = {Cork, Ireland},
PUBLISHER = {Springer},
MONTH = {June},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {3097},
ISBN = {3-540-22345-2},
YEAR = {2004},
PAGES = {168--182},
ABSTRACT = {The paper presents a modular superposition calculus for the
combination of first-order theories involving both total
and partial functions. Modularity means that inferences are
pure, only involving clauses over the alphabet of either
one, but not both, of the theories. The calculus is shown
to be complete provided that functions that are not in the
intersection of the component signatures are declared as
partial. This result also means that if the
unsatisfiability of a goal modulo the combined theory does
not depend on the totality of the functions in the
extensions, the inconsistency will be effectively found.
Moreover, we consider a constraint superposition calculus
for the case of hierarchical theories and show that it has
a related modularity property. Finally we identify cases
where the partial models can always be made total so that
modular superposition is also complete with respect to the
standard (total function) semantics of the theories.},
}
@INPROCEEDINGS{GanzingerHillenbrandWaldmann2003,
AUTHOR = {Ganzinger, Harald and Hillenbrand, Thomas and Waldmann, Uwe},
EDITOR = {Baader, Franz},
TITLE = {Superposition modulo a {Shostak} Theory},
BOOKTITLE = {Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction},
PADDRESS = {Berlin, Germany},
ADDRESS = {Miami, Florida},
PUBLISHER = {Springer},
MONTH = {July},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {2741},
ISBN = {3-540-40559-3},
YEAR = {2003},
PAGES = {182--196},
ABSTRACT = { We investigate superposition modulo a Shostak theory $T$ in order to
facilitate reasoning in the amalgamation of $T$ and a free
theory~$F$.
%
Free operators occur naturally e.\,g.\ in program verification
problems when abstracting over subroutines. If their behaviour in
addition can be specified axiomatically, much more of the program
semantics can be captured.
%
Combining the Shostak-style components for deciding the clausal
validity problem with the ordering and saturation techniques
developed for equational reasoning, we derive a refutationally
complete calculus on mixed ground clauses which result for example
from CNF transforming arbitrary universally quantified formulae.
%
The calculus works modulo a Shostak theory in the sense that it
operates on canonizer normalforms. For the Shostak solvers that we
study, coherence comes for free: no coherence pairs need to be
considered.},
}
@INPROCEEDINGS{GanzingerKorovin-03-lics,
AUTHOR = {Ganzinger, Harald and Korovin, Konstantin},
EDITOR = {Kolaitis, Phokion},
TITLE = {New Directions in Instantiation-Based Theorem Proving},
BOOKTITLE = {18th Annual IEEE Symposium on Logic in Computer Science (LICS-03)},
ORGANIZATION = {Institute of Electrical and Electronics Engineers (IEEE)},
PADDRESS = {Los Alamitos, USA},
ADDRESS = {Ottawa, Canada},
PUBLISHER = {IEEE},
ISBN = {0-7695-1884-2},
YEAR = {2003},
PAGES = {55--64},
ABSTRACT = {We consider instantiation-based theorem proving whereby
instances of clauses are generated by certain inferences, and where
inconsistency is detected by propositional tests.
We give a model construction proof of completeness by which restrictive
inference
systems as well as admissible simplification techniques can be
justified. Another contribution of the paper are novel inference
systems that allow one to also employ decision procedures for
first-order fragments more complex than propositional logic.
The decision procedure provides for an approximative consistency test, and the
instance generation inference system is a means of
successively refining the approximation.},
}
@INPROCEEDINGS{GanzingerMeyerWeidenbach-97-cade,
AUTHOR = {Ganzinger, Harald and Meyer, Christoph and Weidenbach, Christoph},
EDITOR = {McCune, William},
TITLE = {Soft Typing for Ordered Resolution},
BOOKTITLE = {Proceedings of the 14th International Conference on Automated Deduction (CADE-14)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Townsville, Australia},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1249},
ISBN = {3-540-63104-6},
YEAR = {1997},
PAGES = {321--335},
ABSTRACT = {We propose a variant of ordered resolution with semantic restrictions
based on interpretations which are identified by the given atom ordering
and selection function. Techniques for effectively approximating validity
in these interpretations are described that are related to methods of
soft typing for programming languages.
The framework is shown to be strictly more general than certain related
methods.
Implementation in the \spass\ prover has lead to encouraging experimental
results.},
}
@INPROCEEDINGS{GanzingerSofronie-Stokkermans-00-ismvl,
AUTHOR = {Ganzinger, Harald and Sofronie-Stokkermans, Viorica},
TITLE = {Chaining Techniques for Automated Theorem Proving in Many-Valued Logics},
BOOKTITLE = {Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL-00)},
ORGANIZATION = {IEEE Computer Society Technical Committee on Multiple-Valued Logic; Oregon Center for Advanced Technology Education},
PADDRESS = {Los Alamitos, USA},
ADDRESS = {Portland, Oregon},
PUBLISHER = {IEEE},
ISBN = {0-7695-0692-5},
YEAR = {2000},
PAGES = {337--344},
ABSTRACT = {We apply chaining techniques to automated theorem proving in many-valued
logics. In particular, we show that superposition specializes to a refined
version of the many-valued resolution rules introduced by Baaz and Ferm{\"u}ller,
and that ordered chaining can be specialized to a refutationally complete
inference system for regular clauses.},
}
@INPROCEEDINGS{GanzingerWaldmann-92-ctrs,
AUTHOR = {Ganzinger, Harald and Waldmann, Uwe},
EDITOR = {Rusinowitch, M. and R{\'e}my, J.-L.},
TITLE = {Termination Proofs of Well-Moded Logic Programs Via Conditional Rewrite Systems},
BOOKTITLE = {Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems '92},
PADDRESS = {Berlin, Germany},
ADDRESS = {?},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {656},
YEAR = {1992},
PAGES = {430--437},
ABSTRACT = {In this paper, it is shown that a translation from logic programs to
conditional rewrite rules can be used in a straightforward way to check
(semi-automatically) whether a program is terminating under the prolog
selection rule.},
}
@INPROCEEDINGS{GanzingerWaldmann1996CADE,
AUTHOR = {Ganzinger, Harald and Waldmann, Uwe},
EDITOR = {McRobbie, Michael A. and Slaney, John K.},
TITLE = {Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)},
BOOKTITLE = {Proceedings of the 13th International Conference on Automated Deduction (CADE-13)},
PADDRESS = {Berlin, Germany},
ADDRESS = {New Brunswick, USA},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1104},
ISBN = {3-540-61511-3},
YEAR = {1996},
PAGES = {388--402},
NOTE = {Full version:
Technical Report MPI-I-96-2-001,
Max-Planck-Institut f{\"u}r Informatik, Saarbr{\"u}cken, Germany,
January 1996.},
ABSTRACT = {Cancellative abelian monoids encompass abelian groups,
but also such ubiquitous structures as the natural numbers or
multisets. Both the AC axioms and the cancellation law are
difficult for a general purpose theorem prover, as they create
many variants of clauses which contain sums. We describe a
refined superposition calculus for cancellative abelian monoids
which requires neither explicit inferences with the theory clauses
nor extended equations or clauses. Strong ordering constraints
allow us to restrict to inferences that involve the maximal term
of the maximal sum in the maximal literal. Besides, the search
space is reduced drastically by variable elimination techniques.},
}
@INPROCEEDINGS{Gasse-Sofronie-Stokkermans-dl2011,
AUTHOR = {Gasse, Francis and Sofronie-Stokkermans, Viorica},
EDITOR = {Rosati, Riccardo and Rudolph, Sebastian and Zakharyaschev, Michael},
TITLE = {Efficient {TBox} Subsumption Checking in Combinations of {EL} and (fragments of) {FL0}},
BOOKTITLE = {Proceedings of the 2011 International Workshop on Description Logics (DL-2011)},
PADDRESS = {Aachen, Germany},
ADDRESS = {Barcelona, Spain},
PUBLISHER = {CEUR Workshop Proceedings},
MONTH = {June},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {745},
YEAR = {2011},
PAGES = {125--135},
ABSTRACT = {We study possibilities of combining (fragments) of the lightweight description
logics ${\cal F}{\cal L}_0$ and
${\cal E}{\cal L}$, and identify classes of subsumption
problems in a combination of ${\cal E}{\cal L}$ and
Horn-${\cal F}{\cal L}_0$, which can be
checked in PSPACE resp. PTIME.
Since ${\cal F}{\cal L}_0$ allows universal role restrictions
and ${\cal E}{\cal L}$ allows existential role restrictions,
we thus have a framework where subsumption between
expressions including both types
of role restrictions (but for disjoint sets of roles) can be checked in
polynomial
space or time.},
}
@ARTICLE{GSW-i-and-c,
AUTHOR = {Ganzinger, Harald and Sofronie-Stokkermans, Viorica and Waldmann, Uwe},
JOURNAL = {Information and Computation},
TITLE = {Modular Proof Systems for Partial Functions with {Evans} Equality},
NUMBER = {10},
PUBLISHER = {Elsevier},
MONTH = {October},
VOLUME = {204},
ISBN = {0890-5401},
YEAR = {2006},
PAGES = {1453--1492},
ABSTRACT = {The paper presents a modular superposition calculus for the
combination of first-order theories involving both total
and partial functions. Modularity means that inferences are
pure, only involving clauses over the alphabet of either
one, but not both, of the theories. The calculus is shown
to be complete provided that functions that are not in the
intersection of the component signatures are declared as
partial. This result also means that if the
unsatisfiability of a goal modulo the combined theory does
not depend on the totality of the functions in the
extensions, the inconsistency will be effectively found.
Moreover, we consider a constraint superposition calculus
for the case of hierarchical theories and show that it has
a related modularity property. Finally we identify cases
where the partial models can always be made total so that
modular superposition is also complete with respect to the
standard (total function) semantics of the theories.},
}
@TECHREPORT{HaehnleKerberEtAl96,
AUTHOR = {H{\"a}hnle, Reiner and Kerber, Manfred and Weidenbach, Christoph},
TITLE = {{Common Syntax of the DFG-Schwerpunktprogramm ``Deduktion''}},
INSTITUTION = {Universit{\"a}t Karlsruhe},
TYPE = {Interner Bericht},
ADDRESS = {Karlsruhe, Fakult{\"a}t f{\"u}r Informatik, Germany},
NUMBER = {10/96},
MONTH = {April},
YEAR = {1996},
PAGES = {10},
}
@INPROCEEDINGS{Hillenbrand2003,
AUTHOR = {Hillenbrand, Thomas},
EDITOR = {Dahn, Ingo and Vigneron, Laurent},
TITLE = {Citius altius fortius: Lessons learned from the Theorem Prover {WALDMEISTER}},
BOOKTITLE = {Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03},
TYPE = {Invited Talk},
PADDRESS = {Amsterdam, The Netherlands},
ADDRESS = {Valencia, Spain},
PUBLISHER = {Elsevier},
MONTH = {June},
SERIES = {Electronic Notes in Theoretical Computer Science},
VOLUME = {86.1},
YEAR = {2003},
PAGES = {1--13},
ABSTRACT = {In the last years, the development of automated theorem
provers has been advancing in a so to speak Olympic spirit,
following the motto "faster, higher, stronger"; and the
{Waldmeister} system has been a part of that endeavour. We
will survey the concepts underlying this prover, which
implements Knuth-Bendix completion in its unfailing variant.
The system architecture is based on a strict separation of
active and passive facts, and is realized via specifically
tailored representations for each of the central data
structures: indexing for the active facts, set-based
compression for the passive facts, successor sets for the
conjectures. In order to cope with large search spaces,
specialized redundancy criteria are employed, and the
empirically gained control knowledge is integrated to ease
the use of the system. We conclude with a discussion of
strengths and weaknesses, and a view of future prospects.},
}
@INPROCEEDINGS{Hillenbrand2004,
AUTHOR = {Hillenbrand, Thomas},
EDITOR = {Sattler, Ulrike},
TITLE = {A Superposition View on {Nelson-Oppen}},
BOOKTITLE = {Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning},
PADDRESS = {Aachen},
ADDRESS = {Cork, Ireland},
PUBLISHER = {CEUR},
MONTH = {July},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {106},
ISBN = {1613-0073},
YEAR = {2004},
PAGES = {16--20},
}
@PHDTHESIS{HillenbrandDiss2008,
AUTHOR = {Hillenbrand, Thomas},
TITLE = {Superposition and Decision Procedures -- Back and Forth},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Doctoral dissertation},
MONTH = {October},
YEAR = {2008},
ABSTRACT = {Two apparently different approaches to automating deduction are mentioned in
the title; they are the subject of a debate on ``big engines vs.\ little
engines of proof''. The contributions in this thesis advocate that these two
strands of research can interplay in subtle and sometimes unexpected ways, such
that mutual pervasion can lead to intriguing results: Firstly, superposition
can be run on top of decision procedures. This we demonstrate for the class of
Shostak theories, incorporating a little engine into a big one. As another
instance of decision procedures within superposition, we show that ground
confluent rewrite systems, which decide entailment problems in equational
logic, can be harnessed for detecting redundancies in superposition
derivations. Secondly, superposition can be employed as proof-theoretic means
underneath combined decision procedures: We re-establish the correctness of the
Nelson-Oppen procedure as an instance of the completeness of superposition.
Thirdly, superposition can be used as a decision procedure for many interesting
theories, turning a big engine into a little one. For the theory of bits and of
fixed-size bitvectors, we suggest a rephrased axiomatization combined with a
transformation of conjectures, based on which superposition decides the
universal fragment. Furthermore, with a modification of lifting, we adapt
superposition to the theory of bounded domains and give a decision procedure,
which captures the Bernays-Sch\"onfinkel class as well.},
}
@INPROCEEDINGS{HillenbrandEtAl2006Disproving,
AUTHOR = {Hillenbrand, Thomas and Topic, Dalibor and Weidenbach, Christoph},
EDITOR = {de Nivelle, Hans},
TITLE = {Sudokus as Logical Puzzles},
BOOKTITLE = {Disproving'06: Non-Theorems, Non-Validity, Non-Provability},
PADDRESS = {Seattle, USA},
ADDRESS = {Seattle, USA},
PUBLISHER = {Self publishing},
MONTH = {August},
YEAR = {2006},
PAGES = {2--12},
}
@INPROCEEDINGS{HillenbrandLoechner2001,
AUTHOR = {Hillenbrand, Thomas and L{\"o}chner, Bernd},
EDITOR = {de Nivelle, Hans and Schulz, Stephan},
TITLE = {The Next {WALDMEISTER} Loop (Extended Abstract)},
BOOKTITLE = {Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001},
PADDRESS = {Saarbr{\"u}cken, Germany},
ADDRESS = {Havana, Cuba},
PUBLISHER = {Max-Planck-Institut f{\"u}r Informatik},
MONTH = {November},
SERIES = {Research Report},
VOLUME = {MPI-I-2001-2-006},
YEAR = {2001},
PAGES = {13--21},
}
@INCOLLECTION{HillenbrandPiskacWaldmannWeidenbach2011,
AUTHOR = {Hillenbrand, Thomas and Piskac, Ruzica and Waldmann, Uwe and Weidenbach, Christoph},
EDITOR = {Voronkov, Andrei and Weidenbach, Christoph},
TITLE = {From Search to Computation: Redundancy Criteria and Simplification at Work},
BOOKTITLE = {Programming Logics, Essays in Memory of Harald Ganzinger},
ADDRESS = {Berlin},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7797},
YEAR = {2013},
}
@INCOLLECTION{HillenbrandWeidenbach13,
AUTHOR = {Hillenbrand, Thomas and Weidenbach, Christoph},
EDITOR = {Bonacina, Maria Paola and Stickel, Mark},
TITLE = {Superposition for Bounded Domains},
BOOKTITLE = {Automated Reasoning and Mathematics, Essays in Memory of William W. McCune},
ADDRESS = {Heidelberg},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7788},
YEAR = {2013},
PAGES = {68--100},
}
@TECHREPORT{HillenbrandWeidenbach2007Report,
AUTHOR = {Hillenbrand, Thomas and Weidenbach, Christoph},
TITLE = {Superposition for Finite Domains},
INSTITUTION = {Max-Planck Institute for Informatics},
TYPE = {Research Report},
ADDRESS = {Saarbruecken, Germany},
NUMBER = {MPI-I-2007-RG1-002},
MONTH = {April},
YEAR = {2007},
PAGES = {25},
}
@MASTERSTHESIS{Hirt2006,
AUTHOR = {Hirth, Simon},
TITLE = {{Automatische Analyse von DHCP und h{\"o}heren Infrasturkturdiensten mit SPASS}},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
MONTH = {July},
YEAR = {2006},
}
@TECHREPORT{HirthKarlWeidenbach2007report,
AUTHOR = {Hirth, Simon and Karl, Carsten and Weidenbach, Christoph},
TITLE = {Automatic Analysis of {LAN} Infrastructures},
INSTITUTION = {Max Planck Institute for Informatics},
TYPE = {Research Report},
ADDRESS = {Saarbruecken, Germany},
NUMBER = {MPI-I-2007-RG1-001},
YEAR = {2007},
PAGES = {160},
}
@INPROCEEDINGS{HL02-CADE18,
AUTHOR = {Hillenbrand, Thomas and L{\"o}chner, Bernd},
EDITOR = {Voronkov, Andrei},
TITLE = {The Next {WALDMEISTER} Loop},
BOOKTITLE = {Automated deduction, CADE-18 : 18th International Conference on Automated Deduction},
PADDRESS = {Heidelberg, Germany},
ADDRESS = {Copenhagen, Denmark},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {2392},
ISBN = {3-540-43931-5},
YEAR = {2002},
PAGES = {486--500},
ABSTRACT = { In saturation-based theorem provers, the reasoning process consists
in constructing the closure of an axiom set under inferences. As is
well-known, this process tends to quickly fill the memory available
unless preventive measures are employed. For implementations based
on the DISCOUNT loop, the passive facts are responsible for most
of the memory consumption. We present a refinement of that loop
allowing such a compression that the space needed for the passive
facts is linearly bound by the number of active facts. In practice,
this will reduce memory consumption in the WALDMEISTER system by
more than one order of magnitude as compared to previous compression
schemes.},
}
@TECHREPORT{Horbach2009TR1,
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
TITLE = {Deciding the Inductive Validity of Forall Exists* Queries},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
TYPE = {Research Report},
ADDRESS = {Saarbr{\"u}cken},
NUMBER = {MPI-I-2009-RG1-001},
MONTH = {May},
YEAR = {2009},
PAGES = {48},
ABSTRACT = {We present a new saturation-based decidability result for inductive validity.
Let $\Sigma$ be a finite signature in which all function symbols are at most
unary and let $N$ be a satisfiable Horn clause set without equality in which
all positive literals are linear.
If $N\cup\{A_1,\ldots,A_n\rightarrow\}$ belongs to a finitely saturating clause
class, then it is decidable whether a sentence of the form $\forall\exists^*
(A_1\wedge\ldots\wedge A_n)$ is valid in the minimal model of $N$.},
}
@TECHREPORT{Horbach2009TR2,
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
TITLE = {Superposition for Fixed Domains},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
TYPE = {Research Report},
ADDRESS = {Saarbr{\"u}cken},
NUMBER = {MPI-I-2009-RG1-005},
MONTH = {October},
ISBN = {0946-011X},
YEAR = {2009},
PAGES = {49},
ABSTRACT = {Superposition is an established decision procedure for a variety of first-order
logic theories represented by sets of clauses. A satisfiable theory, saturated
by superposition, implicitly defines a minimal term-generated model for the
theory.
Proving universal properties with respect to a saturated theory directly leads
to a modification of the minimal model's term-generated domain, as new Skolem
functions are introduced. For many applications, this is not desired.
Therefore, we propose the first superposition calculus that can explicitly
represent existentially quantified variables and can thus compute with respect
to a given domain. This calculus is sound and refutationally complete in the
limit for a first-order fixed domain semantics.
For saturated Horn theories and classes of positive formulas, we can even
employ the calculus to prove properties of the minimal model itself, going
beyond the scope of known superposition-based approaches.},
}
@INPROCEEDINGS{Horbach2010,
AUTHOR = {Horbach, Matthias},
EDITOR = {Clarke, Edmund M. and Voronkov, Andrei},
TITLE = {Disunification for Ultimately Periodic Interpretations},
BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16},
PADDRESS = {Berlin},
ADDRESS = {Dakar, Senegal},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6355},
ISBN = {978-3-642-17510-7},
DOI = {10.1007/978-3-642-17511-4_17},
YEAR = {2010},
PAGES = {290--311},
}
@PHDTHESIS{Horbach2010PhD,
AUTHOR = {Horbach, Matthias},
TITLE = {Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Doctoral dissertation},
ADDRESS = {Saarbr{\"u}cken},
PUBLISHER = {Universit{\"a}t des Saarlandes},
MONTH = {July},
YEAR = {2010},
PAGES = {186},
ABSTRACT = {Superposition is an established decision procedure for a variety of first-order
logic theories represented by sets of clauses. A satisfiable theory, saturated
by superposition, implicitly defines a minimal Herbrand model for the theory.
This raises the question in how far superposition calculi can be employed for
reasoning about such minimal models. This is indeed often possible when
existential properties are considered. However, proving universal properties
directly leads to a modification of the minimal model's term-generated domain,
as new Skolem functions are introduced. For many applications, this is not
desired because it changes the problem.
In this thesis, I propose the first superposition calculus that can explicitly
represent existentially quantified variables and can thus compute with respect
to a given fixed domain. It does not eliminate existential variables by
Skolemization, but handles them using additional constraints with which each
clause is annotated. This calculus is sound and refutationally complete in the
limit for a fixed domain semantics. For saturated Horn theories and classes of
positive formulas, the calculus is even complete for proving properties of the
minimal model itself, going beyond the scope of known superposition-based
approaches.
The calculus is applicable to every set of clauses with equality and does not
rely on any syntactic restrictions of the input. Extensions of the calculus
lead to various new decision procedures for minimal model validity. A main
feature of these decision procedures is that even the validity of queries
containing one quantifier alternation can be decided. In particular, I prove
that the validity of any formula with at most one quantifier alternation is
decidable in models represented by a finite set of atoms and that the validity
of several classes of such formulas is decidable in models represented by
so-called disjunctions of implicit generalizations. Moreover, I show that the
decision of minimal model validity can be reduced to the superposition-based
decision of first-order validity for models of a class of predicative Horn
clauses where all function symbols are at most unary.},
}
@BOOK{Horbach2013Informatik,
AUTHOR = {Horbach, Matthias},
EDITOR = {Horbach, Matthias},
TITLE = {INFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und Umwelt},
ADDRESS = {Bonn-Buschdorf},
PUBLISHER = {K{\"o}llen},
MONTH = {September},
SERIES = {Lecture Notes in Informatics},
VOLUME = {P-220},
ISBN = {978-3-88579-614-5},
YEAR = {2013},
PAGES = {3148},
}
@INCOLLECTION{Horbach2013McCune,
AUTHOR = {Kapur, Deepak and Zhang, Zhihai and Horbach, Matthias and Zhao, Hantao and Lu, Qi and Nguyen, ThanhVu},
EDITOR = {Bonacina, Maria Paola and Stickel, Mark E.},
TITLE = {Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants},
BOOKTITLE = {Automated Reasoning and Mathematics: Essays in Memory of William McCune},
ADDRESS = {Berlin},
PUBLISHER = {Springer},
SERIES = {LNAI},
VOLUME = {7788},
YEAR = {2014},
PAGES = {189--228},
ABSTRACT = {Geometric heuristics for the quantifier elimination approach presented by Kapur
(2004) are investigated to automatically derive loop invariants expressing
weakly relational numerical properties (such as $l \le x \le h$ or $l \le \pm x
\pm y \leq h$) for imperative programs.
Such properties have been successfully used to analyze commercial software
consisting of hundreds of thousands of lines of code (using for example, the
Astr\'ee tool based on abstract interpretation framework proposed by Cousot and
his group).
The main attraction of the proposed approach is its much lower
complexity in contrast to the abstract interpretation approach ($O(n^2)$ in
contrast to $O(n^4)$, where $n$ is the number of variables) with the ability to
still generate invariants of comparable strength.
This approach has been generalized to consider disjunctive invariants of the
similar form, expressed using maximum function (such as $\max(x+a,y+b,z+c,d)
\le \max(x+e,y+f,z+g,h)$), thus enabling automatic generation of a subclass of
disjunctive
invariants for imperative programs as well.},
}
@INPROCEEDINGS{HorbachWeidenbach2009CADE,
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
EDITOR = {Schmidt, Renate A.},
TITLE = {Decidability Results for Saturation-Based Model Building},
BOOKTITLE = {Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction},
PADDRESS = {Berlin, Germany},
ADDRESS = {Montreal, Canada},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {5663},
ISBN = {978-3-642-02958-5},
DOI = {0.1007/978-3-642-02959-2_30},
YEAR = {2009},
PAGES = {404--420},
ABSTRACT = {Saturation-based calculi such as superposition can be successfully instantiated
to decision procedures for many decidable fragments of first-order logic. In
case of termination without generating an empty clause, a saturated clause set
implicitly represents a minimal model for all clauses, based on the underlying
term ordering of the superposition calculus. In general, it is not decidable
whether a ground atom, a clause or even a formula holds in this minimal model
of a satisfiable saturated clause set.
We extend our superposition calculus for fixed domains with syntactic
disequality constraints in a non-equational setting. Based on this calculus, we
present several new decidability results for validity in the minimal model of a
satisfiable finitely saturated clause set that in particular extend the
decidability results known for ARM (Atomic Representations of term Models) and
DIG (Disjunctions of Implicit Generalizations) model representations.},
}
@ARTICLE{HorbachWeidenbach2010,
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
JOURNAL = {ACM Transactions on Computational Logic},
TITLE = {Superposition for Fixed Domains},
ADDRESS = {New York, NY},
NUMBER = {4},
PUBLISHER = {ACM},
MONTH = {November},
VOLUME = {11},
ISBN = {1529-3785},
DOI = {10.1145/1805950.1805957},
YEAR = {2010},
PAGES = {27,1--27,35},
ABSTRACT = {Disunification is an extension of unification to first-order formulae over
syntactic equality atoms. Instead of considering only syntactic equality, I
extend a disunification algorithm by Comon and Delor to ultimately periodic
interpretations, i.e.~minimal many-sorted Herbrand models of predicative Horn
clauses and, for some sorts, equations of the form $s^\upmb(x)\eq s^\upma(x)$.
The extended algorithm is terminating and correct for ultimately periodic
interpretations over a finite signature and gives rise to a decision procedure
for the satisfiability of equational formulae in ultimately periodic
interpretations.
As an application, I show how to apply disunification to compute the completion
of predicates with respect to an ultimately periodic interpretation. Such
completions are a key ingredient to several inductionless induction methods.},
}
@INPROCEEDINGS{HorbachWeidenbachCSL08,
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
TITLE = {Superposition for Fixed Domains},
BOOKTITLE = {CSL},
PADDRESS = {Berlin/Heidelberg},
ADDRESS = {Bertinoro, Italy},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {5213},
ISBN = {978-3-540-87530-7},
YEAR = {2008},
PAGES = {293--307},
}
@INPROCEEDINGS{HorbachWeidenbachCSL09,
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
EDITOR = {Gr{\"a}del, Erich and Kahle, Reinhard},
TITLE = {Deciding the Inductive Validity of {FOR} {ALL} {THERE} {EXISTS*} Queries},
BOOKTITLE = {Computer Science Logic : 23rd International Workshop, CSL 2009, 18th Annual Conference of the EACSL},
PADDRESS = {Berlin, Germany},
ADDRESS = {Coimbra, Portugal},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {5771},
ISBN = {978-3-642-04026-9},
DOI = {10.1007/978-3-642-04027-6_25},
YEAR = {2009},
PAGES = {332--347},
}
@INPROCEEDINGS{hpilot2009,
AUTHOR = {Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
EDITOR = {Schmidt, Renate A.},
TITLE = {System Description: {H-PILoT}},
BOOKTITLE = {Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction},
PADDRESS = {Berlin, Germany},
ADDRESS = {Montreal, Canada},
PUBLISHER = {Springer},
MONTH = {August},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {5663},
ISBN = {978-3-642-02958-5},
DOI = {10.1007/978-3-642-02959-2_9},
YEAR = {2009},
PAGES = {131--139},
ABSTRACT = {H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions)
is a program for hierarchical reasoning in extensions of logical theories with
additional functions axiomatized by a set of (universally quantified) clauses:
deduction problems in the theory extension are reduced to deduction problems
in the base theory. Specialized provers, as well as standard SMT solvers, are
then used for testing the satisfiability of the formulae obtained after the
reduction. The hierarchical reduction used in H-PILoT is always sound; it
is complete for the class of so-called local extensions of a base theory.
If the clauses obtained by this reduction belong to a fragment decidable in
the base theory, H-PILoT provides a decision procedure for testing
satisfiability of ground formulae w.r.t.\ a theory extension, and can also
be used for model generation. This is the major advantage of H-PILoT compared
with other state-of-the art SMT solvers. H-PILoT can alternatively be used as
a tool for ``steering'' the instantiation mechanism of standard SMT provers,
in order to provide decision procedures in the case of local theory extensions.
This system description provides an overview of H-PILoT and illustrates on
some examples the main advantage of using H-PILoT for satisfiability
checking in local extensions, in comparison with the performance of general
state of the art SMT-provers.},
}
@INPROCEEDINGS{HPT02,
AUTHOR = {Hillenbrand, Thomas and Podelski, Andreas and Topi{\'c}, Dalibor},
EDITOR = {Charatonik, Witold and Ganzinger, Harald},
TITLE = {Is Logic Effective for Analyzing {C} Programs?},
BOOKTITLE = {Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi},
PADDRESS = {Saarbr{\"u}cken, Germany},
ADDRESS = {Saarbr{\"u}cken},
PUBLISHER = {Max-Planck-Institut f{\"u}r Informatik},
MONTH = {March},
SERIES = {MPI Research Report},
VOLUME = {MPI-I-2002-2-007},
YEAR = {2002},
PAGES = {27--30},
}
@INPROCEEDINGS{HSW1998,
AUTHOR = {Hustadt, Ullrich and Schmidt, Renate A. and Weidenbach, Christoph},
EDITOR = {de Swart, Harrie},
TITLE = {Optimised Functional Translation and Resolution},
BOOKTITLE = {Proceedings of the International Conference on Automated Reaso ning with Analytic Tableaux and Related Methods (TABLEAUX'98)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Oisterwijk, The Netherlands},
PUBLISHER = {Springer},
MONTH = {May},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1397},
ISBN = {3-540-64406-7},
YEAR = {1998},
PAGES = {36--37},
}
@INPROCEEDINGS{ihlemann-jacobs-sofronie-tacas2008,
AUTHOR = {Ihlemann, Carsten and Jacobs, Swen and Sofronie-Stokkermans, Viorica},
EDITOR = {Ramakrishnan, C. R. and Rehof, Jakob},
TITLE = {On local reasoning in verification},
BOOKTITLE = {Proceedings of TACAS 2008},
PADDRESS = {New York},
ADDRESS = {Budapest, Hungary},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4963},
YEAR = {2008},
PAGES = {265--281},
ABSTRACT = {We present a general framework which allows to identify complex theories
important in verification for which efficient reasoning methods exist. The
framework we present is based on a general notion of locality. We show that
locality considerations allow us to obtain parameterized decidability and
complexity results for many (combinations of) theories important in
verification in general and in the verification of parametric systems in
particular. We give numerous examples; in particular we show that several
theories of data structures studied in the verification literature are local
extensions of a base theory. The general framework we use allows us to identify
situations in which some of the syntactical restrictions imposed in previous
papers can be relaxed.},
}
@TECHREPORT{Ihlemann-Sofronie-Stokkermans-atr60-2010,
AUTHOR = {Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
EDITOR = {Bernd, Becker and Damm, Werner and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {On hierarchical reasoning in combinations of theories},
INSTITUTION = {Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)},
TYPE = {Technical Report},
ADDRESS = {Saarbr{\"u}cken},
NUMBER = {ATR 60},
MONTH = {August},
ISBN = {1860-9821},
YEAR = {2010},
PAGES = {26},
ABSTRACT = {In this paper we study theory combinations over non-disjoint
signatures in which hierarchical and modular reasoning is
possible. We use a notion of locality of a theory extension
parameterized by a closure operator on ground terms.
We give criteria for recognizing these types of theory
extensions. We then show that combinations of extensions of
theories which are local in this extended sense have also a
locality property and hence allow modular and hierarchical
reasoning. We thus obtain parameterized decidability and
complexity results for many (combinations of) theories
important in verification.},
}
@TECHREPORT{Ihlemann-Sofronie-Stokkermans-atr61-2010,
AUTHOR = {Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
EDITOR = {Bernd, Becker and Damm, Werner and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {System Description: {H-PILoT} (Version 1.9)},
INSTITUTION = {Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)},
TYPE = {Technical Report},
ADDRESS = {Saarbr{\"u}cken},
NUMBER = {ATR 61},
MONTH = {August},
ISBN = {1860-9821},
YEAR = {2010},
PAGES = {45},
ABSTRACT = {This system description provides an overview of H-PILoT
(Hierarchical Proving by Instantiation in Local Theory
extensions), a program for hierarchical reasoning in
extensions of logical theories.
H-PILoT reduces deduction problems in the theory extension
to deduction problems in the base theory.
Specialized provers and standard SMT solvers can be used
for testing the satisfiability of the formulae obtained
after the reduction. For a certain type of theory extension
(namely for {\em local theory extensions}) this
hierarchical reduction is sound and complete and --
if the formulae obtained this way belong to a fragment
decidable in the base theory -- H-PILoT provides a decision
procedure for testing satisfiability of ground formulae,
and can also be used for model generation.},
}
@INPROCEEDINGS{Ihlemann-Sofronie-Stokkermans-ijcar-2010,
AUTHOR = {Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
EDITOR = {Giesl, J{\"u}rgen and H{\"a}hnle, Reiner},
TITLE = {On Hierarchical Reasoning in Combinations of Theories},
BOOKTITLE = {Automated Reasoning : 5th International Joint Conference, IJCAR 2010},
PADDRESS = {Berlin},
ADDRESS = {Edinburgh},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6173},
ISBN = {978-3-642-14202-4},
DOI = {10.1007/978-3-642-14203-1_4},
YEAR = {2010},
PAGES = {30--45},
ABSTRACT = {In this paper we study theory combinations over non-disjoint
signatures in which hierarchical and modular reasoning is
possible. We use a notion of locality of a theory extension
parameterized by a closure operator on ground terms.
We give criteria for recognizing these types of theory
extensions. We then show that combinations of extensions of
theories which are local in this extended sense also have a
locality property and hence allow modular and hierarchical
reasoning. We thus obtain parameterized decidability and
complexity results for many (combinations of) theories
important in verification.},
}
@PHDTHESIS{IhlemannDiss2010,
AUTHOR = {Ihlemann, Carsten},
TITLE = {Reasoning in Combinations of Theories},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Doctoral dissertation},
ADDRESS = {Saarbr{\"u}cken},
PUBLISHER = {Universit{\"a}t des Saarlandes},
MONTH = {August},
YEAR = {2010},
PAGES = {176},
ABSTRACT = {\section*{Abstract}
Verification problems are often expressed in a language which mixes several
theories.
A natural question to ask is whether one can use decision procedures for
individual theories to construct a decision procedure for the union theory.
In the cases where this is possible one has a powerful method at hand to handle
complex theories effectively.
The setup considered in this thesis is that of one base theory which is
extended by one or more theories.
The question is if and when a given ground satisfiability problem in the
extended setting can be
effectively reduced to an equi-satisfiable
problem
over the base theory. A case where this reductive approach is always possible
is that of so-called \emph{local theory extensions.}
The theory of local extensions is developed and some applications concerning
monotone functions are given.
Then the theory of local theory extensions is generalized in order to deal with
data structures that
exhibit local behavior.
It will be shown that a suitable fragment of both the theory of arrays and the
theory of pointers
is local in this broader sense.
%
Finally, the case of more than one theory extension is discussed.
In particular, a \emph{modularity} result is given that under certain
circumstances the locality of each of the extensions
lifts to locality of the entire extension.
The reductive approach outlined above has become particularly relevant
in recent years due to the rise of powerful solvers for background
theories common in verification tasks. These so-called SMT-solvers
effectively handle theories such as real linear or integer arithmetic.
As part of this thesis, a program called \emph{\mbox{H-PILoT}} was
implemented which carries out reductive reasoning for local theory
extensions. H-PILoT found applications in mathematics, multiple-valued
logics, data-structures and reasoning in complex systems.
},
}
@INPROCEEDINGS{jacobs-sofronie-pdpar-06,
AUTHOR = {Jacobs, Swen and Sofronie-Stokkermans, Viorica},
EDITOR = {Cook, Byron and Sebastiani, Roberto},
TITLE = {Applications of hierarchical reasoning in the verification of complex systems},
BOOKTITLE = {PDPAR'06: Pragmatical Aspects of Decision Procedures in Automated Reasoning},
PADDRESS = {-},
ADDRESS = {Seattle, USA},
MONTH = {August},
YEAR = {2006},
PAGES = {15--26},
ABSTRACT = {In this paper we show how hierarchical reasoning can be
used to verify properties of complex systems. Chains of
local theory extensions are used to model a case study
taken from the European Train Control System (ETCS)
standard, but considerably simplified. We show how
testing invariants and bounded model checking can
automatically be reduced to checking satisfiability
of ground formulae over a base theory.},
}
@ARTICLE{jacobs-sofronie-pdpar-entcs,
AUTHOR = {Jacobs, Swen and Sofronie-Stokkermans, Viorica},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
TITLE = {Applications of hierarchical reasoning in the verification of complex systems},
NUMBER = {8},
PUBLISHER = {Elsevier},
VOLUME = {174},
ISBN = {1571-0661},
DOI = {10.1016/j.entcs.2006.11.038},
YEAR = {2007},
PAGES = {39--54},
ABSTRACT = {In this paper we show how hierarchical reasoning can be
used to verify properties of complex systems.
Chains of local theory extensions are used to model a case
study taken from the European Train Control System (ETCS)
standard, but considerably simplified. We show how testing
invariants and bounded model checking (for safety properties
expressed by universally quantified formulae,
depending on certain parameters of the systems)
can automatically be reduced to checking
satisfiability of ground formulae over a base theory. },
}
@INPROCEEDINGS{Jacobs2008,
AUTHOR = {Jacobs, Swen},
EDITOR = {Baader, Franz and Ghilardi, Silvio and Hermann, Miki and Sattler, Ulrike and Sofronie-Stokkermans, Viorica},
TITLE = {Incremental Instance Generation in Local Reasoning},
BOOKTITLE = {Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08},
PADDRESS = {Sydney, Australia},
ADDRESS = {Sydney, Australia},
MONTH = {August},
YEAR = {2008},
PAGES = {47--62},
ABSTRACT = {Local reasoning allows to handle SMT problems involving a certain class of
universally quantified formulas in a complete way by instantiation to a finite
set of ground formulas. We present a method to generate this set incrementally,
in order to provide a more efficient way of solving these satisfiability
problems. The incremental instantiation is guided semantically, inspired by the
instance generation approach to first-order theorem proving. Our method is
sound and complete, and terminates on both satisfiable and unsatisfiable input
after generating a subset of the instances needed in standard local reasoning.},
}
@INPROCEEDINGS{Jacobs2009,
AUTHOR = {Jacobs, Swen},
EDITOR = {Bouajjani, Ahmed and Maler, Oded},
TITLE = {Incremental Instance Generation in Local Reasoning},
BOOKTITLE = {Computer Aided Verification : 21st International Conference, CAV 2009},
PADDRESS = {Berlin, Germany},
ADDRESS = {Grenoble, France},
PUBLISHER = {Springer},
MONTH = {June},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {5643},
ISBN = {978-3-642-02657-7},
DOI = {10.1007/978-3-642-02658-4_29},
YEAR = {2009},
PAGES = {368--382},
ABSTRACT = {Many verification approaches use SMT solvers in some form, and are limited by
their incomplete handling of quantified formulas. Local reasoning allows to
handle SMT problems involving a certain class of
universally quantified formulas in a complete way by instantiation to a finite
set of ground formulas. We present a method to generate these instances
incrementally, in order to provide a more efficient way of solving these
satisfiability problems. The incremental instantiation is guided semantically,
inspired by the instance generation approach to first-order theorem proving. Our
method is sound and complete, and terminates on both satisfiable and
unsatisfiable input after generating a subset of the instances needed in
standard local reasoning. Experimental results show that for a large class of
examples the incremental approach is substantially more efficient than eager
generation of all instances.},
}
@PHDTHESIS{JacobsDiss2010,
AUTHOR = {Jacobs, Swen},
TITLE = {Hierarchic Decision Procedures for Verification},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Doctoral dissertation},
MONTH = {January},
YEAR = {2010},
PAGES = {133},
}
@INPROCEEDINGS{JacobsWaldmann2005,
AUTHOR = {Jacobs, Swen and Waldmann, Uwe},
EDITOR = {Beckert, Bernhard},
TITLE = {Comparing Instance Generation Methods for Automated Reasoning},
BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2005},
PADDRESS = {Berlin, Germany},
ADDRESS = {Koblenz, Germany},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {3702},
ISBN = {3-540-28931-3},
YEAR = {2005},
PAGES = {153--168},
ABSTRACT = {The clause linking technique of Lee and Plaisted
proves the unsatisfiability
of a set of first-order clauses
by generating a sufficiently large set of instances of these clauses
that can be shown to be propositionally unsatisfiable.
In recent years,
this approach has been refined in several directions,
leading to both tableau-based methods,
such as the Disconnection Tableau Calculus,
and saturation-based methods,
such as Primal Partial Instantiation
and Resolution-based Instance Generation.
We investigate the relationship between these calculi
and answer the question to what extent
refutation or consistency proofs in one calculus
can be simulated in another one.},
}
@ARTICLE{JacobsWaldmann2006,
AUTHOR = {Jacobs, Swen and Waldmann, Uwe},
JOURNAL = {Journal of Automated Reasoning},
TITLE = {Comparing Instance Generation Methods for Automated Reasoning},
ADDRESS = {Netherlands},
PUBLISHER = {Springer},
MONTH = {December},
VOLUME = {38},
ISBN = {0168-7433},
YEAR = {2006},
PAGES = {57--78},
NOTE = {"Online First" version of 2007 journal article},
ABSTRACT = {The clause-linking technique of Lee and Plaisted proves the unsatisfiability of
a set of first-order clauses by generating a sufficiently large set of
instances of these clauses that can be shown to be propositionally
unsatisfiable. In recent years, this approach has been refined in several
directions, leading to both tableau-based methods, such as the disconnection
tableau calculus, and saturation-based methods, such as primal partial
instantiation and resolution-based instance generation. We investigate the
relationship between these calculi and answer the question to what extent
refutation or consistency proofs in one calculus can be simulated in another
one.},
}
@ARTICLE{JacobsWaldmann2007,
AUTHOR = {Jacobs, Swen and Waldmann, Uwe},
JOURNAL = {Journal of Automated Reasoning},
TITLE = {Comparing Instance Generation Methods for Automated Reasoning},
NUMBER = {1/3},
PUBLISHER = {Springer},
MONTH = {April},
VOLUME = {38},
ISBN = {0168-7433},
DOI = {10.1007/s10817-006-9046-x},
YEAR = {2007},
PAGES = {57--78},
ABSTRACT = {The clause-linking technique of Lee and Plaisted proves the unsatisfiability of
a set of first-order clauses by generating a sufficiently large set of
instances of these clauses that can be shown to be propositionally
unsatisfiable. In recent years, this approach has been refined in several
directions, leading to both tableau-based methods, such as the disconnection
tableau calculus, and saturation-based methods, such as primal partial
instantiation and resolution-based instance generation. We investigate the
relationship between these calculi and answer the question to what extent
refutation or consistency proofs in one calculus can be simulated in another
one.},
}
@INPROCEEDINGS{JacquemardMeyerWeidenbach98,
AUTHOR = {Jacquemard, Florent and Meyer, Christoph and Weidenbach, Christoph},
EDITOR = {Nipkow, Tobias},
TITLE = {Unification in Extensions of Shallow Equational Theories},
BOOKTITLE = {Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Tsukuba, Japan},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1379},
ISBN = {3-540-64301-X},
YEAR = {1998},
PAGES = {76--90},
ABSTRACT = {We show that unification in certain extensions of shallow equational theories
is decidable. Our extensions generalize the known classes of
shallow or standard equational theories. In order to prove decidability of
unification in the extensions, a class of Horn clause sets called sorted
shallow equational theories is introduced. This class is a natural extension of
tree automata with equality constraints between brother subterms as
well as shallow sort theories. We show that saturation under sorted
superposition is effective on sorted shallow equational theories. So called
semi-linear equational theories can be effectively transformed into equivalent
sorted shallow equational theories and generalize the classes of
shallow and standard equational theories. },
}
@MASTERSTHESIS{Karl2006,
AUTHOR = {Karl, Carsten},
TITLE = {{Automatische Analyse von Layer 3 Netzwerken mit SPASS}},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
MONTH = {July},
YEAR = {2006},
}
@INPROCEEDINGS{KarrenbergKostaSturm2013,
AUTHOR = {Karrenberg, Ralf and Ko{\v{s}}ta, Marek and Sturm, Thomas},
EDITOR = {Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt},
TITLE = {Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages},
BOOKTITLE = {Frontiers of Combining Systems},
PADDRESS = {Berlin},
ADDRESS = {Nancy, France},
PUBLISHER = {Springer},
MONTH = {September},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {8152},
ISBN = {978-3-642-40884-7},
DOI = {10.1007/978-3-642-40885-4_5},
YEAR = {2013},
PAGES = {56--70},
ABSTRACT = {Data-parallel languages like OpenCL and CUDA are an important means to exploit
the computational power of today's computing devices.
We consider the compilation of such languages for CPUs with SIMD instruction
sets.
To generate efficient code, one wants to statically decide whether or not
certain
memory operations access consecutive addresses.
We formalize the notion of consecutivity and algorithmically reduce the static
decision to satisfiability problems in Presburger Arithmetic.
We introduce a preprocessing technique on these SMT problems, which makes it
feasible to apply an off-the-shelf SMT solver.
We show that a prototypical OpenCL CPU driver based on our approach generates
more efficient code than any other state-of-the-art driver.},
}
@INPROCEEDINGS{Kosta2013,
AUTHOR = {Ko{\v{s}}ta, Marek},
EDITOR = {Ko{\v{s}}ta, Marek and Sturm, Thomas},
TITLE = {{SMT}-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages},
BOOKTITLE = {Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences},
PADDRESS = {Nanning},
ADDRESS = {Nanning, China},
YEAR = {2013},
PAGES = {36--42},
}
@MASTERSTHESIS{Kruglov2008,
AUTHOR = {Kruglov, Evgeny},
TITLE = {Superposition Modulo Linear Arithmetic},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
MONTH = {March},
YEAR = {2008},
}
@PHDTHESIS{KruglovDiss13,
AUTHOR = {Kruglov, Evgeny},
TITLE = {Superposition Modulo Theory},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Doctoral dissertation},
MONTH = {October},
YEAR = {2013},
}
@INPROCEEDINGS{KruglovFroCoS2011,
AUTHOR = {Eggers, Andreas and Kruglov, Evgeny and Kupferschmid, Stefan and Scheibler, Karsten and Teige, Teige and Weidenbach, Christoph},
EDITOR = {Sofronie-Stokkermans, Viorica and Tinelli, Cesare},
TITLE = {{SUP(NLA)} -- Combining Superposition and Non-Linear Arithmetic},
BOOKTITLE = {8th International Symposium on Frontiers of Combining Systems},
PADDRESS = {Heidelberg},
ADDRESS = {Saarbruecken, Germany},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6989},
ISBN = {978-3-642-24363-9},
YEAR = {2011},
PAGES = {119--134},
ABSTRACT = {The first-order theory over non-linear arithmetic
including transcendental functions (NLA) is undecidable.
Nevertheless, in this paper we show that a particular combination
with superposition leads to a sound and complete calculus that
is useful in practice. We follow basically the ideas
of the SUP(LA) combination, but have to take care
of undecidability, resulting in ``unknown'' answers by
the NLA reasoning procedure. A pipeline
of NLA constraint simplification techniques related to
the SUP(NLA) framework significantly decreases the number of ``unknown''
answers.
The resulting approach is implemented as SUP(NLA) by a system combination
of SPASS and iSAT. Applied to various scenarios
of traffic collision avoidance protocols, we show by experiments
that SPASS(iSAT) can fully automatically proof and disproof safety
properties of such protocols using the very same formalization.},
}
@INPROCEEDINGS{KruglovMACIS2011,
AUTHOR = {Kruglov, Evgeny and Weidenbach, Christoph},
EDITOR = {Ratschan, Stefan},
TITLE = {{SUP(T)} Decides First-Order Logic Fragment Over Ground Theories},
BOOKTITLE = {Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS-4)},
PADDRESS = {Beijing, China},
ADDRESS = {Beijing, China},
PUBLISHER = {Internal Conference Proceedings},
YEAR = {2011},
ABSTRACT = {The hierarchic superposition calculus SUP(T) enables sound reasoning on the
hierarchic combination of a theory T with full first-order logic FOL(T). If a
FOL(T) clause set enjoys a sufficient completeness criterion, the calculus is
even complete. Clause sets over the ground fragment of FOL(T) are not
sufficiently complete, in general. In this paper we show that any clause set
over the ground FOL(T) fragment can be transformed into a sufficiently complete
one, and prove that SUP(T) is terminating for the transformed clause set, hence
a decision procedure provided the existential fragment of the theory T is
decidable. Thanks to the hierarchic design of SUP(T), the decidability result
can be extended beyond the ground case. We show SUP(T) is a decision procedure
for the non-ground FOL fragment plus a theory T, if every non-constant function
symbol from the underlying FOL signature ranges into the sort of the theory T,
and every term of the theory sort is ground. Examples for T are in particular
decidable fragments of arithmetic.},
}
@ARTICLE{KruglovWeidenbachMCS2012,
AUTHOR = {Kruglov, Evgeny and Weidenbach, Christoph},
JOURNAL = {Mathematics in Computer Science},
TITLE = {Superposition Decides the First-Order Logic Fragment Over Ground Theories},
ADDRESS = {Basel},
NUMBER = {4},
PUBLISHER = {Birkh{\"a}user},
MONTH = {December},
VOLUME = {6},
ISBN = {1661-8270},
DOI = {10.1007/s11786-012-0135-4},
YEAR = {2012},
PAGES = {427--456},
ABSTRACT = {The hierarchic superposition calculus over a theory T, called SUP(T), enables
sound reasoning on the hierarchic combination
of a theory T with full first-order logic, FOL(T). If a FOL(T) clause set
enjoys a sufficient completeness criterion,
the calculus is even complete. Clause sets over the ground fragment of FOL(T)
are not sufficiently complete, in general.
In this paper we show that any clause set over the ground FOL(T) fragment can
be transformed into a sufficiently complete one,
and prove that SUP(T) terminates on the transformed clause set, hence
constitutes a decision procedure provided the
existential fragment of the theory T is decidable. Thanks to the hierarchic
design of SUP(T), the decidability result
can be extended beyond the ground case. We show SUP(T) is a decision procedure
for the non-ground FOL fragment
plus a theory T, if every non-constant function symbol from the underlying FOL
signature ranges into the sort of the theory T,
and every term of the theory sort is ground. Examples for T are in particular
decidable fragments of arithmetic.},
}
@ARTICLE{KruglovWeidenbachMCS2012e,
AUTHOR = {Kruglov, Evgeny and Weidenbach, Christoph},
JOURNAL = {Mathematics in Computer Science},
TITLE = {Superposition Decides the First-Order Logic Fragment Over Ground Theories},
ADDRESS = {Basel},
NUMBER = {4},
PUBLISHER = {Birkh{\"a}user},
MONTH = {December},
VOLUME = {6},
ISBN = {1661-8289},
DOI = {10.1007/s11786-012-0135-4},
YEAR = {2012},
PAGES = {427--456},
ABSTRACT = {The hierarchic superposition calculus over a theory T, called SUP(T), enables
sound reasoning on the hierarchic combination
of a theory T with full first-order logic, FOL(T). If a FOL(T) clause set
enjoys a sufficient completeness criterion,
the calculus is even complete. Clause sets over the ground fragment of FOL(T)
are not sufficiently complete, in general.
In this paper we show that any clause set over the ground FOL(T) fragment can
be transformed into a sufficiently complete one,
and prove that SUP(T) terminates on the transformed clause set, hence
constitutes a decision procedure provided the
existential fragment of the theory T is decidable. Thanks to the hierarchic
design of SUP(T), the decidability result
can be extended beyond the ground case. We show SUP(T) is a decision procedure
for the non-ground FOL fragment
plus a theory T, if every non-constant function symbol from the underlying FOL
signature ranges into the sort of the theory T,
and every term of the theory sort is ground. Examples for T are in particular
decidable fragments of arithmetic.},
}
@INPROCEEDINGS{Lamotte-SchubertWeidenbachFTP09,
AUTHOR = {Lamotte-Schubert, Manuel and Weidenbach, Christoph},
EDITOR = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
TITLE = {Analysis of Authorizations in {SAP} {R/3}},
BOOKTITLE = {First-order Theorem Proving, FTP 2009 : International Workshop on First-Order Theorem Proving proceedings},
ORGANIZATION = {University of Oslo},
PADDRESS = {Oslo, Norway},
ADDRESS = {Oslo, Norway},
PUBLISHER = {University of Oslo/Department of Informatics},
MONTH = {July},
SERIES = {University Oslo/Departmant of Informatics: Research Report},
VOLUME = {386},
ISBN = {82-7368-347-8},
YEAR = {2009},
PAGES = {90--104},
ABSTRACT = {Today many companies use an ERP (Enterprise Resource Planning) system
such as SAP R/3~to run their daily business ranging from
financial issues down to the actual control of a production line.
Already due to their sheer size, these systems are very complex.
In particular, developing and maintaining the authorization setup
is a challenge.
The goal of our effort is to automatically analyze the authorization
setup of an SAP R/3~system against business policies.
To this end we formalize the processes, authorization setup
as well as the business policies
in first-order logic. Then, properties can be (dis)proven fully automatically
with our theorem prover \textsc{Spass}. We exemplify our approach
on the purchase process, a typical constituent of any SAP R/3~installation.},
}
@INPROCEEDINGS{Lamotte-SchubertWeidenbachFTP09CEUR,
AUTHOR = {Lamotte-Schubert, Manuel and Weidenbach, Christoph},
EDITOR = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
TITLE = {Analysis of Authorizations in {SAP} {R/3}},
BOOKTITLE = {FTP 2009 : First-Order Theorem Proving},
PADDRESS = {s.l.},
ADDRESS = {Oslo, Norway},
PUBLISHER = {CEUR},
MONTH = {July},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {556},
YEAR = {2009},
PAGES = {90--104},
ABSTRACT = {Today many companies use an ERP (Enterprise Resource Planning) system such as
SAP R/3 to run their daily business ranging from financial issues down to the
actual control of a production line. Already due to their sheer size, these
systems are very complex. In particular, developing and maintaining the
authorization setup is a challenge. The goal of our effort is to automatically
analyze the authorization setup of an SAP R/3 system against business policies.
To this end we formalize the processes, authorization setup as well as the
business policies in first-order logic. Then, properties can be (dis)proven
fully automatically with our theorem prover Spass. We exemplify our approach
on the purchase process, a typical constituent of any SAP R/3 installation.},
}
@MASTERSTHESIS{LAMOTTE2008,
AUTHOR = {Lamotte, Manuel},
TITLE = {{Analysis of Authorizations in SAP R/3}},
SCHOOL = {Fachhochschule Trier},
TYPE = {Master's thesis},
PUBLISHER = {Self publishing},
MONTH = {January},
YEAR = {2008},
ABSTRACT = {Today many companies use an ERP (Enterprise Resource Planning) system
such as the SAP R/3 system to run their daily business ranging from
financial issues down to the actual control of a production line.
These systems are very complex from the view of administration and
authorization. Hence they include a high potential for errors. In this
thesis I analyze the authorization concept of the SAP R/3 system as well as
different business regulations and construct a corresponding model
in first-order logic. This model can be used to check the existence
of errors automatically, i.e. a contradiction between given authorizations
and a valid business regulation. The tool I use for these checks
is the theorem prover \textsc{Spass} which has been developed at the
Max Planck Institute for Informatics. I selected the purchase process as an
example
to explore the model construction because it is a typical constituent of the
SAP R/3 system.},
}
@INPROCEEDINGS{LasarukSturm:11a,
AUTHOR = {Lasaruk, Aless and Sturm, Thomas},
EDITOR = {Sturm, Thomas and Zengler, Christoph},
TITLE = {Automatic Verification of the Adequacy of Models for Families of Geometric Objects},
BOOKTITLE = {Automated Deduction in Geometry : 7th International Workshop, ADG 2008},
PADDRESS = {Berlin},
ADDRESS = {Shanghai, China},
PUBLISHER = {Springer},
MONTH = {May},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6301},
ISBN = {978-3-642-21045-7},
DOI = {10.1007/978-3-642-21046-4_6},
YEAR = {2011},
PAGES = {116--140},
ABSTRACT = {We consider parametric families of semi-algebraic geometric objects, each
implicitly defined by a first-order formula. Given an unambiguous description
of such an object family and an intended alternative description we
automatically construct a first-order formula which is true if and only if our
alternative description uniquely describes geometric objects of the reference
description. We can decide this formula by applying real quantifier
elimination. In the positive case we furthermore derive the defining
first-order formulas corresponding to our new description. In the negative case
we can produce sample points establishing a counterexample for the uniqueness.
We demonstrate our method by automatically proving uniqueness theorems for
characterizations of several geometric primitives and simple complex objects.
Finally, we focus on tori, characterizations of which can be applied in spline
approximation theory with toric segments. Although we cannot yet practically
solve the fundamental open questions in this area within reasonable time and
space, we demonstrate that they can be formulated in our framework. In addition
this points at an interesting and practically relevant challenge problem for
automated deduction in geometry in general.},
}
@ARTICLE{LetzWeidenbach98,
AUTHOR = {Letz, Reinhold and Weidenbach, Christoph},
JOURNAL = {KI, Organ des Fachbereichs 1 "K{\"u}nstliche Intelligenz'' der Gesellschaft f{\"u}r Informatik e.V.},
TITLE = {{Paradigmen und Perspektiven der automatischen Deduktion}},
VOLUME = {4},
YEAR = {1998},
PAGES = {15--19},
}
@INPROCEEDINGS{LevAmiWeidenbachEtAl2007CADE,
AUTHOR = {Lev-Ami, Tal and Weidenbach, Christoph and Reps, Thomas and Sagiv, Mooly},
TITLE = {Labelled Clauses},
BOOKTITLE = {21st International Conference on Automated Deduction (CADE-21)},
PADDRESS = {New York},
ADDRESS = {Bremen, Germany},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4603},
YEAR = {2007},
PAGES = {311--327},
}
@ARTICLE{LoechnerHillenbrandAICOM2002,
AUTHOR = {L{\"o}chner, Bernd and Hillenbrand, Thomas},
JOURNAL = {AI Communications},
TITLE = {A Phytography of {WALDMEISTER}},
ADDRESS = {Amsterdam, the Netherlands},
NUMBER = {2-3},
PUBLISHER = {IOS Press},
MONTH = {August},
VOLUME = {15},
ISBN = {0921-7126},
YEAR = {2002},
PAGES = {127--133},
ABSTRACT = {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.},
}
@PHDTHESIS{LuDiss13,
AUTHOR = {Lu, Tianxiang},
TITLE = {Formal Verification of the Pastry Protocol},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Doctoral dissertation},
MONTH = {November},
YEAR = {2013},
}
@MASTERSTHESIS{LudwigDipl2006,
AUTHOR = {Ludwig, Michel},
TITLE = {Extensions of the {Knuth-Bendix} Ordering with {LPO}-like Properties},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
MONTH = {July},
YEAR = {2006},
ABSTRACT = {The Lexicographic Path Order (LPO) and the Knuth-Bendix
Ordering (KBO) are two prominent term orders that are
utilised in automated theorem provers. The LPO features
some properties that allow it to be used in the context
of hierarchic signature extensions and in the presence
of term definitions, where special ordering criteria are
desired for the defined terms. The KBO, on the other
hand, can be computed more efficiently than the LPO and
it correlates better with the size of terms, but the KBO
cannot be used in the afore-mentioned situations, in
which a single term should supersede infinitely many
smaller terms of arbitrary sizes. In this diploma
thesis, we present two extensions of the KBO that
overcome these limitations. The first extension order is
suitable for hierarchic signature extensions and its
main characteristic is that it uses pairs of positive
real numbers as symbol weights, whereas the second
extension can handle the required ordering of term
definitions through the usage of ordinal numbers as
symbol weights.},
}
@INPROCEEDINGS{LudwigWaldmann2007,
AUTHOR = {Ludwig, Michel and Waldmann, Uwe},
EDITOR = {Dershowitz, Nachum and Voronkov, Andrei},
TITLE = {An Extension of the {Knuth-Bendix} Ordering with {LPO}-Like Properties},
BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007},
PADDRESS = {Berlin, Germany},
ADDRESS = {Yerevan, Armenia},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {4790},
ISBN = {3-540-75558-6},
YEAR = {2007},
PAGES = {348--362},
ABSTRACT = {The Knuth-Bendix ordering is usually preferred over the
lexicographic path ordering in successful implementations
of resolution and superposition, but it is incompatible
with certain requirements of hierarchic superposition
calculi. Moreover, it does not allow non-linear definition
equations to be oriented in a natural way. We present
an extension of the Knuth-Bendix ordering that makes it
possible to overcome these restrictions.},
}
@INPROCEEDINGS{LuTlaPastryForte2011,
AUTHOR = {Lu, Tianxiang and Merz, Stephan and Weidenbach, Christoph},
EDITOR = {Bruni, Roberto and Dingel, Juergen},
TITLE = {Towards Verification of the {Pastry} Routing Protocol using {TLA}+},
BOOKTITLE = {Formal Techniques for Distributed Systems : Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011 and 30th IFIP WG 6.1 International Conference, FORTE 2011},
PADDRESS = {Berlin},
ADDRESS = {Reykjavik, Iceland},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {6722},
ISBN = {978-3-642-21460-8},
DOI = {10.1007/978-3-642-21461-5_16},
YEAR = {2011},
PAGES = {244--258},
NOTE = {Accepted },
}
@INPROCEEDINGS{LuTX2009,
AUTHOR = {Lu, Tianxiang and Merz, Stephan and Weidenbach, Christoph},
EDITOR = {Bendisposto, Jens and Leuschel, Michael and Roggenbach, Markus},
TITLE = {Model Checking the {Pastry} Routing Protocol},
BOOKTITLE = {10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010)},
ORGANIZATION = {Microsoft Research},
PADDRESS = {D{\"u}sseldorf},
ADDRESS = {D{\"u}sseldorf, Germany},
PUBLISHER = {Universit{\"a}t D{\"u}sseldorf},
MONTH = {September},
YEAR = {2010},
PAGES = {19--21},
ABSTRACT = {Pastry is an algorithm for implementing a scalable distributed hash table over
an underlying P2P network, an active area of research in distributed systems.
Several implementations of Pastry are available and have been applied in
practice, but no attempt has so far been made to formally describe the
algorithm or to verify its properties. Since Pastry combines rather complex
data structures, asynchronous communication, concurrency, resilience to
\emph{churn} and fault tolerance, it makes an interesting target for
verification. We have modeled Pastry's core routing algorithms in the
specification language \texorpdfstring{\textrm{\upshape
TLA\textsuperscript{+}}}{TLA+} and used its model checker \textsc{tlc} to
analyze qualitative properties of Pastry such as \emph{correctness} and
\emph{consistency}.},
}
@MASTERSTHESIS{Neumann09,
AUTHOR = {Neumann, Stephan Rouven},
TITLE = {Automated Proof Generation of Possibiltiy Properties in Inductive Protocol Verification},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Bachelor thesis},
ADDRESS = {Saarbr{\"u}cken},
PUBLISHER = {Universit{\"a}t des Saarlandes},
MONTH = {April},
YEAR = {2009},
}
@INPROCEEDINGS{NieuwenhuisHillenbrandRiazanovVoronkov2001,
AUTHOR = {Nieuwenhuis, Robert and Hillenbrand, Thomas and Riazanov, Alexandre and Voronkov, Andrei},
EDITOR = {Gor{\'e}, Rajeev and Leitsch, Alexander and Nipkow, Tobias},
TITLE = {On the Evaluation of Indexing Techniques for Theorem Proving},
BOOKTITLE = {Automated reasoning : First International Joint Conference, IJCAR 2001},
PADDRESS = {Berlin, Germany},
ADDRESS = {Siena, Italy},
PUBLISHER = {Springer},
MONTH = {June},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {2083},
ISBN = {3-540-42254-5},
YEAR = {2001},
PAGES = {257--271},
}
@INPROCEEDINGS{NonnengartRockWeidenbach98,
AUTHOR = {Nonnengart, Andreas and Rock, Georg and Weidenbach, Christoph},
EDITOR = {Kirchner, Claude and Kirchner, H{\'e}l{\`e}ne},
TITLE = {On Generating Small Clause Normal Forms},
BOOKTITLE = {Proceedings of the 15th International Conference on Automated Deduction (CADE-98)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Lindau, Germany},
PUBLISHER = {Springer},
MONTH = {July},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1421},
ISBN = {3-540-64675-2},
YEAR = {1998},
PAGES = {397--411},
ABSTRACT = {In this paper we focus on two powerful techniques to obtain compact clause
normal forms:
Renaming of formulae and refined Skolemization methods.
We illustrate their effect on various examples.
By an exhaustive experiment of all first-order TPTP problems,
it shows that our clause normal form transformation yields fewer clauses and
fewer literals
than the methods known and used so far.
This often allows for exponentially shorter proofs and,
in some cases, it makes it even possible for a theorem prover to find a proof
where it was
unable to do so with more standard clause normal form transformations.},
}
@INCOLLECTION{NonnengartWeidenbach2001handbook,
AUTHOR = {Nonnengart, Andreas and Weidenbach, Christoph},
EDITOR = {Robinson, Alan and Voronkov, Andrei},
TITLE = {Computing small clause normal forms},
BOOKTITLE = {Handbook of Automated Reasoning},
CHAPTER = {6},
ADDRESS = {Amsterdam, the Netherlands},
PUBLISHER = {Elsevier},
MONTH = {January},
VOLUME = {1},
YEAR = {2001},
PAGES = {335--367},
}
@ARTICLE{OhlbachWeidenbach95,
AUTHOR = {Ohlbach, Hans J{\"u}rgen and Weidenbach, Christoph},
JOURNAL = {Journal of Automated Reasoning},
TITLE = {A Note on Assumptions about Skolem Functions},
NUMBER = {2},
PUBLISHER = {Kluwer},
VOLUME = {15},
ISBN = {0168-7433},
YEAR = {1995},
PAGES = {267--275},
ABSTRACT = {Skolemization is not an equivalence preserving transformation. For the
purposes of refutational theorem proving it is sufficient that
Skolemization preserves satisfiability and unsatisfiability. Therefore
there is sometimes some freedom in interpreting Skolem functions in a
particular way. We show that in certain cases it is possible to
exploit this freedom for simplifying formulae considerably. Examples for cases
where
this occurs systematically are the relational translation from modal
logics to predicate logic and the relativization of first-order logics with
sorts.},
}
@PROCEEDINGS{Peltier-Sofronie-Stokkermans-ftpceur-2010,
EDITOR = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
TITLE = {First-Order Theorem Proving 2009},
PADDRESS = {Aachen},
ADDRESS = {Oslo, Norway},
PUBLISHER = {Nicolas Peltier and Viorica Sofronie-Stokkermans (on CEUR-WS)},
SERIES = {CEUR-WS},
VOLUME = {556},
YEAR = {2009},
PAGES = {1--139},
}
@INPROCEEDINGS{PrevostoWaldmann2006,
AUTHOR = {Prevosto, Virgile and Waldmann, Uwe},
EDITOR = {Sutcliffe, Geoff and Schmidt, Renate and Schulz, Stephan},
TITLE = {{SPASS+T}},
BOOKTITLE = {ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning},
PADDRESS = {-},
ADDRESS = {Seattle, WA, USA},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {192},
ISBN = {1613-0073},
YEAR = {2006},
PAGES = {18--33},
ABSTRACT = {SPASS+T is an extension of the superposition-based theorem prover SPASS that
allows us to enlarge the reasoning capabilities of SPASS using an arbitrary SMT
procedure for arithmetic and free function symbols as a black-box. We discuss
the architecture of SPASS+T and the capabilities, limitations, and applications
of such a combination.},
}
@MASTERSTHESIS{Reuter13,
AUTHOR = {Reuter, Jochen},
TITLE = {Real Linear Quantifier Elimination},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
YEAR = {2013},
}
@MASTERSTHESIS{RusevMaster2008,
AUTHOR = {Rusev, Rostislav},
TITLE = {Bitvector Reasoning with SPASS},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
MONTH = {May},
YEAR = {2008},
}
@TECHREPORT{Rybalchenko-Sofronie-Stokkermans-2009,
AUTHOR = {Rybalchenko, Andrey and Sofronie-Stokkermans, Viorica},
EDITOR = {Becker, Bernd and Damm, Werner Martin and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {Constraint Solving for Interpolation},
INSTITUTION = {SFB/TR 14 AVACS},
TYPE = {Technical Report},
ADDRESS = {SFB/TR 14 AVACS},
NUMBER = {ATR 56},
MONTH = {September},
YEAR = {2009},
PAGES = {26},
}
@INPROCEEDINGS{Rybalchenko-Sofronie-vmcai07,
AUTHOR = {Rybalchenko, Andrey and Sofronie-Stokkermans, Viorica},
EDITOR = {Cook, Byron and Podelski, Andreas},
TITLE = {Constraint Solving for Interpolation},
BOOKTITLE = {Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007},
PADDRESS = {Berlin, Germany},
ADDRESS = {Nice, France},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4349},
ISBN = {978-3-540-69735-0},
DOI = {10.1007/978-3-540-69738-1_25},
YEAR = {2007},
PAGES = {346--362},
ABSTRACT = {Interpolation is an important component of recent methods for
program verification. It provides a natural and effective means
for computing separation between the sets of `good' and `bad'
states. The existing algorithms for interpolant generation are
proof-based: They require explicit construction of proofs,
from which interpolants can be computed.
Construction of such proofs is a difficult task.
We propose an algorithm for the generation of interpolants
for the combined theory of linear arithmetic and uninterpreted
function symbols that does not require a priori constructed
proofs to derive interpolants. It uses a reduction of
the problem to constraint solving in linear arithmetic,
which allows application of existing highly optimized Linear
Programming solvers in black-box fashion.
We provide experimental evidence of the practical
applicability of our algorithm.},
}
@INPROCEEDINGS{Sofronie-cade-05,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Nieuwenhuis, Robert},
TITLE = {Hierarchic reasoning in local theory extensions},
BOOKTITLE = {Automated deduction - CADE-20 : 20th International Conference on Automated Deduction},
PADDRESS = {Berlin, Germany},
ADDRESS = {Tallinn, Estonia},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {3632},
ISBN = {0302-9743},
YEAR = {2005},
PAGES = {219--234},
ABSTRACT = {We show that for special types of extensions of a base theory,
which we call {\em local},
efficient hierarchic reasoning is possible.
We identify situations in which it is possible,
for an extension ${\cal T}_1$ of a theory ${\cal T}_0$,
to express the decidability and complexity of the
universal theory of ${\cal T}_1$ in terms of
the decidability resp.\ complexity of suitable
fragments of the theory ${\cal T}_0$ (universal or $\forall \exists$).
These results apply to theories related to data types,
but also to certain theories of functions from mathematics.},
}
@ARTICLE{Sofronie-getco06-entcs,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
TITLE = {Sheaves and geometric logic and applications to modular verification of complex systems},
ADDRESS = {Amsterdam, The Netherlands},
PUBLISHER = {Elsevier},
MONTH = {March},
VOLUME = {230},
ISBN = {1571-0661},
DOI = {10.1016/j.entcs.2009.02.024},
YEAR = {2009},
PAGES = {161--187},
ABSTRACT = {In this paper we show that states, transitions and behavior of
concurrent systems can often be modeled as sheaves over a
suitable topological space.
In this context, geometric logic can be used to describe which
local properties, of individual systems, are preserved, at a
global level, when interconnecting the systems.
The main area of application is to modular verification
of complex systems. We illustrate our ideas by means of an
example involving a family of interacting controllers for
trains on a rail track.},
}
@INPROCEEDINGS{sofronie-ihlemann-ismvl-2007,
AUTHOR = {Sofronie-Stokkermans, Viorica and Ihlemann, Carsten},
TITLE = {Automated reasoning in some local extensions of ordered structures},
BOOKTITLE = {Proceedings of ISMVL 2007},
PADDRESS = {New York},
ADDRESS = {Oslo, Norway},
PUBLISHER = {IEEE},
ISBN = {0-7695-2831-7},
DOI = {10.1109/ISMVL.2007.10},
YEAR = {2007},
PAGES = {Article1},
ABSTRACT = {We give a uniform method for automated reasoning in
several types of extensions of ordered algebraic structures
(definitional extensions, extensions with boundedness
axioms or with monotonicity axioms). We show that such
extensions are local and, hence, efficient methods for
hierarchical reasoning exist in all these cases.},
}
@INPROCEEDINGS{Sofronie-Ihlemann-Jacobs-dagstuhl07,
AUTHOR = {Sofronie-Stokkermans, Viorica and Ihlemann, Carsten and Jacobs, Swen},
EDITOR = {Baader, Franz and Cook, Byron and Giesl, J{\"u}rgen and Nieuwenhuis, Robert},
TITLE = {Local Theory Extensions, Hierarchical Reasoning and Applications to Verification},
BOOKTITLE = {Deduction and Decision Procedures},
TYPE = {Extended Abstract},
PADDRESS = {Dagstuhl, Germany},
ADDRESS = {Dagstuhl, Germany},
PUBLISHER = {Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
MONTH = {December},
SERIES = {Dagstuhl Seminar Proceedings},
VOLUME = {07401},
ISBN = {1862-4405},
YEAR = {2007},
PAGES = {1--22},
ABSTRACT = {Many problems occurring in verification can be reduced to
proving the satisfiability of conjunctions of literals in a
background theory. This can be a concrete theory (e.g. the
theory of real or rational numbers), the extension of a
theory with additional functions (free, monotone, or
recursively defined) or a combination of theories. It is
therefore very important to have efficient procedures for
checking the satisfiability of conjunctions of ground
literals in such theories.
We present some new results on hierarchical and modular
reasoning in complex theories, as well as several examples
of application domains in which efficient reasoning is
possible. We show, in particular, that various phenomena
analyzed in the verification literature can be explained
in a unified way using the notion of local theory extension.},
}
@ARTICLE{sofronie-ihlemann-jmvl-2007,
AUTHOR = {Sofronie-Stokkermans, Viorica and Ihlemann, Carsten},
JOURNAL = {Journal of Multiple-Valued Logic and Soft Computing},
TITLE = {Automated reasoning in some local extensions of ordered structures},
NUMBER = {4-6},
PUBLISHER = {Old City Publishing},
VOLUME = {13},
ISBN = {1542-3980},
YEAR = {2007},
PAGES = {397--414},
ABSTRACT = {We give a uniform method for automated reasoning in
several types of extensions of ordered algebraic structures
(definitional extensions, extensions with boundedness
axioms or with monotonicity axioms). We show that such
extensions are local and, hence, efficient methods for
hierarchical reasoning exist in all these cases.},
}
@INPROCEEDINGS{Sofronie-ijcar-06,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Furbach, Ulrich and Shankar, Natarajan},
TITLE = {Interpolation in local theory extensions},
BOOKTITLE = {Proceedings of IJCAR 2006},
PADDRESS = {New York},
ADDRESS = {Seattle, USA},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {4130},
YEAR = {2006},
PAGES = {235--250},
ABSTRACT = {Many problems in mathematics and computer science
(e.g. in verification, or when reasoning in and about
distributed databases) can be reduced to proving the
satisfiability of conjunctions of (ground) literals modulo
a background theory. This theory can, for instance, be the
extension of a base theory with additional functions or a
combination of theories.
It is therefore very important to find efficient methods for
checking the unsatisfiability of ground formulae in such
complex theories. However, it is often equally important
to find local causes for inconsistency. Such information is
usually provided by interpolants.
In this paper we study interpolation in local extensions of a
base theory ${\cal T}_0$. In such extensions efficient
hierarchical reasoning -- in which a prover for the base theory
is used as a black box -- is possible.
We identify situations in which it is possible to obtain
interpolants in a hierarchical manner, by using a prover
and a procedure for generating interpolants in ${\cal T}_0$
as `black-boxes' in order to generate interpolants in the
extension.
We provide several examples of such theories, and discuss
their applications in verification or knowledge representation.},
}
@ARTICLE{Sofronie-Stokkermans-2010-jsc,
AUTHOR = {Rybalchenko, Andrey and Sofronie-Stokkermans, Viorica},
JOURNAL = {Journal of Symbolic Computation},
TITLE = {Constraint Solving for Interpolation},
ADDRESS = {Amsterdam},
NUMBER = {11},
PUBLISHER = {Elsevier},
VOLUME = {45},
ISBN = {0747-7171},
DOI = {101016/j.jsc.2010.06.005},
YEAR = {2010},
PAGES = {1212--1233},
ABSTRACT = {Interpolation is an important component of recent methods for
program verification. It provides a natural and effective means
for computing the separation between the sets of ‘good’ and
‘bad’ states. The existing algorithms for interpolant generation
are proof-based: They require explicit construction of proofs,
from which interpolants can be computed. Construction of such
proofs is a difficult task. We propose an algorithm for the
generation of interpolants for the combined theory of linear
arithmetic and uninterpreted function symbols that does not
require a priori constructed proofs to derive interpolants. It
uses a reduction of the problem to constraint solving in linear
arithmetic, which allows application of existing highly
optimized Linear Programming solvers in a black-box fashion.
We provide experimental evidence of the practical applicability
of our algorithm.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-2013,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Bonacina, Maria Paola},
TITLE = {Hierarchical reasoning and model generation for the verification of parametric hybrid systems},
BOOKTITLE = {Proceedings of the 24th International Conference on Automated Deduction (CADE-24)},
PADDRESS = {Heidelberg},
ADDRESS = {Lake Placid, New York},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {7898},
YEAR = {2013},
PAGES = {360--376},
ABSTRACT = {In this paper we study possibilities of using methods for
hierarchical reasoning in local theory extensions for the
analysis and verification of parametric hybrid systems,
where the parameters can be either constants or functions.
Our goal is to automatically provide guarantees that such
systems satisfy certain safety or invariance conditions.
We first analyze the possibility of automatically generating
such guarantees in the form of constraints on parameters,
then show that we can also synthesise so-called criticality
functions, typically used for proving stability and/or
safety of hybrid systems.
We illustrate our methods on several examples.},
}
@PROCEEDINGS{Sofronie-Stokkermans-addct07,
EDITOR = {Ghilardi, Silvio and Sattler, Ulrike and Sofronie-Stokkermans, Viorica and Tiwari, Ashish},
TITLE = {Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07)},
PADDRESS = {-},
ADDRESS = {Bremen, Germany},
PUBLISHER = {Informal proceedings},
YEAR = {2007},
PAGES = {1--79},
}
@INPROCEEDINGS{Sofronie-Stokkermans-aiml2008,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Areces, Carlos and Goldblatt, Robert},
TITLE = {Locality and subsumption testing in $\mathcal{EL}$ and some of its extensions},
BOOKTITLE = {Advances in Modal Logic, Vol.7 (Proceedings of AIML 2008)},
PADDRESS = {London, UK},
ADDRESS = {Nancy, France},
PUBLISHER = {College Publications},
ISBN = {978-1-904987-68-0},
YEAR = {2008},
PAGES = {315--339},
ABSTRACT = {In this paper we show that subsumption problems in many
lightweight description logics (including ${\cal EL}$)
can be expressed as uniform word problems in classes of
semilattices with monotone operators.
We use possibilities of efficient local reasoning in such
classes of algebras to obtain uniform PTIME decision
procedures for CBox subsumption in ${\cal EL}$ and
extensions thereof. These locality considerations allow
us to present a new family of logics which extend
${\cal EL}$ with $n$-ary roles and numerical domains
and also a new extension of ${\cal EL}^+$.},
}
@TECHREPORT{Sofronie-Stokkermans-atr45-2008,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Becker, Bernd and Damm, Werner Martin and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {Efficient Hierarchical Reasoning about Functions over Numerical Domains},
INSTITUTION = {SFB/TR 14 AVACS},
TYPE = {Reports of SFB/TR 14 AVACS},
ADDRESS = {SFB/TR 14 AVACS},
NUMBER = {ATR 45},
ISBN = {ISSN: 1860-9821},
YEAR = {2008},
PAGES = {19},
NOTE = {extended version of an article with the same name published in
the proceedings of KI 2008.},
ABSTRACT = {We show that many properties studied in mathematical
analysis (monotonicity, boundedness, inverse, Lipschitz
properties, possibly combined with continuity or derivability)
are expressible by formulae in a class for which sound and
complete hierarchical proof methods for testing satisfiability of
sets of ground clauses exist.
The results are useful for automated reasoning in mathematical
analysis and for the verification of hybrid systems.},
}
@TECHREPORT{Sofronie-Stokkermans-atr46-2008,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Becker, Bernd and Damm, Werner Martin and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {Sheaves and geometric logic and applications to modular verification of complex systems},
INSTITUTION = {SFB/TR 14 AVACS},
TYPE = {Reports of SFB/TR 14 AVACS},
ADDRESS = {SFB/TR 14 AVACS},
NUMBER = {ATR 46},
MONTH = {December},
ISBN = {1860-9821},
YEAR = {2008},
PAGES = {43},
ABSTRACT = {In this paper we show that states, transitions and behavior of
concurrent systems can often be modeled as sheaves over a
suitable topological space (where the topology expresses how the
interacting systems share the information). This allows us to use
results from categorical logic (and in particular geometric
logic) to describe which type of properties are transferred, if
valid locally in all component systems, also at a global level,
to the system obtained by interconnecting the individual systems.
The main area of application is to modular verification of
complex systems.
We illustrate the ideas by means of an example involving
a family of interacting controllers for trains on a rail track.},
}
@PROCEEDINGS{Sofronie-Stokkermans-cade-2011,
EDITOR = {Bj{\o}rner, Nikolaj and Sofronie-Stokkermans, Viorica},
TITLE = {Automated Deduction - CADE-23 : 23rd International Conference on Automated Deduction},
PADDRESS = {Berlin},
ADDRESS = {Wroclaw, Poland},
PUBLISHER = {Springer},
MONTH = {July},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6803},
ISBN = {978-3-642-22437-9},
DOI = {10.1007/978-3-642-22438-6},
YEAR = {2011},
PAGES = {1--505},
}
@INPROCEEDINGS{Sofronie-Stokkermans-cade09,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Schmidt, Renate A.},
TITLE = {Locality results for certain extensions of theories with bridging functions},
BOOKTITLE = {Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction},
PADDRESS = {Berlin, Germany},
ADDRESS = {Montreal, Canada},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {5663},
ISBN = {978-3-642-02958-5},
DOI = {10.1007/978-3-642-02959-2_5},
YEAR = {2009},
PAGES = {67--83},
ABSTRACT = {n this paper we study possibilities of reasoning about
functions over theories of data types which satisfy
certain recursion (or homomorphism) properties, with a
focus on emphasizing possibilities of hierarchical and
modular reasoning in such extensions and combinations thereof.
We start by considering theories of absolutely free data
structures, and continue by studying extensions of such
theories with selectors, with functions which attach scalar
data to the data structures and with additional functions
defined using a certain type of recursion axioms (possibly
having values in a different -- e.g.\ numeric -- domain).
We show that in these cases locality results can be established.
This allows us to reduce the task of reasoning about the class
of recursive functions we consider to reasoning in the
underlying theory of absolutely free data structures
(resp. in a combination of the theory of absolutely free data
structures with the theory attached with the domains of the
additional functions). We then show that similar results can be
obtained if we relax some assumptions about the absolute
freeness of the underlying theory of data types. We investigate
the applications of these ideas in verification and cryptography.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-cade2000,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {McAllester, David},
TITLE = {On unification for bounded distributive lattices},
BOOKTITLE = {Proceedings of the 17th International Conference on Automated Deduction (CADE-17)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Pittsburgh, Pennsylvania, USA},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1831},
ISBN = {3-540-67664-3},
YEAR = {2000},
PAGES = {465--481},
ABSTRACT = {We give a resolution-based procedure for deciding unifiability
in the variety of bounded distributive lattices. The main idea
is to use a structure-preserving translation to clause form to
reduce the problem of testing the satisfiability of a unification
problem ${\cal S}$ to the problem of checking the satisfiability
of a set $\Phi_{\cal S}$ of (constrained) clauses. These ideas
can be used for unification with free constants and for
unification with linear constant restrictions. Complexity issues
are also addressed.},
}
@PROCEEDINGS{Sofronie-Stokkermans-cedar2008,
EDITOR = {Baader, Franz and Ghilardi, Silvio and Hermann, Miki and Sattler, Ulrike and Sofronie-Stokkermans, Viorica},
TITLE = {Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08)},
PADDRESS = {-},
ADDRESS = {Sydney, Australia},
PUBLISHER = {Informal proceedings},
YEAR = {2008},
PAGES = {1--79},
}
@PROCEEDINGS{Sofronie-Stokkermans-ceur2010,
EDITOR = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
TITLE = {First-Order Theorem Proving : Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)},
PADDRESS = {Aachen},
ADDRESS = {Oslo, Norway},
PUBLISHER = {CEUR- WS.org},
MONTH = {January},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {556},
YEAR = {2010},
PAGES = {139},
NOTE = {Electronic proceedings of FTP 2009.
Appeared in printed version as Research Report 386,
University of Oslo, Department of Informatics, 2009,
ISBN 82-7368-347-8, ISSN 0806-3036 },
}
@INPROCEEDINGS{Sofronie-Stokkermans-dagstuhl-2010,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Ball, Thomas and Giesl, J{\"u}rgen and H{\"a}hnle, Reiner and Nipkow, Tobias},
TITLE = {Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms-},
BOOKTITLE = {Interaction versus Automation : the two Faces of Deduction},
PADDRESS = {Dagstuhl},
ADDRESS = {Schloss Dagstuhl},
PUBLISHER = {Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik},
SERIES = {Dagstuhl Seminar Proceedings},
VOLUME = {09411},
ISBN = {1862-4405},
YEAR = {2010},
PAGES = {1--33},
ABSTRACT = {We study possibilities of reasoning about extensions of base
theories with functions which satisfy certain recursion and
homomorphism properties. Our focus is on emphasizing
possibilities of hierarchical and modular reasoning in such
extensions and combinations thereof.
\begin{itemize}
\item[(1)] We show that the theory of absolutely free
constructors is local, and locality is preserved also in the
presence of selectors. These results are consistent with
existing decision procedures for this theory (e.g. by Oppen).
\item[(2)] We show that, under certain assumptions, extensions
of the theory of absolutely free constructors with functions
satisfying a certain type of recursion axioms satisfy locality
properties, and show that for functions with values in an
ordered domain we can combine recursive definitions with
boundedness axioms without sacrificing locality. We also address
the problem of only considering models whose data part is
the {em initial} term algebra of such theories.
\item[(3)] We analyze conditions which ensure that similar
results can be obtained if we relax some assumptions about the
absolute freeness of the underlying theory of data types, and
illustrate the ideas on an example from cryptography.
\end{itemize}
The locality results we establish allow us to reduce the task of
reasoning about the class of recursive functions we consider to
reasoning in the underlying theory of data structures (possibly
combined with the theories associated with the co-domains of
the recursive functions).
As a by-product, the methods we use provide a possibility of
presenting in a different light (and in a different form)
locality phenomena studied in cryp-to-gra-phy; we believe that
they will allow to better separate rewriting from proving, and
thus to give simpler proofs. },
}
@ARTICLE{Sofronie-Stokkermans-dam-06,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {Annals of Mathematics and Artificial Intelligence},
TITLE = {Automated theorem proving by resolution in non-classical logics},
NUMBER = {1-4},
PUBLISHER = {Springer},
MONTH = {April},
VOLUME = {49},
ISBN = {0166-218X},
DOI = {10.1007/s10472-007-9051-8},
YEAR = {2007},
PAGES = {221--252},
ABSTRACT = {This paper is an overview of a variety of results,
all centered around a common theme, namely embedding of
non-classical logics into first order logic and resolution
theorem proving.
We present several classes of non-classical logics, many of
which are of great practical relevance in knowledge
representation, which can be translated into tractable and
relatively simple fragments of classical logic.
In this context, we show that refinements of resolution can
often be used successfully for automated theorem proving,
and in many interesting cases yield optimal decision
procedures.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-dl2008,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Baader, Franz and Lutz, Carsten and Motik, Boris},
TITLE = {Locality and subsumption testing in $\mathcal{EL}$ and some of its extensions},
BOOKTITLE = {Proceedings of the 21st International Workshop on Description Logics (DL-2008)},
PADDRESS = {(operated under the umbrella of RWTH Aachen University with the support of Tilburg University)},
ADDRESS = {Dresden, Germany},
PUBLISHER = {CEUR Workshop Proceedings},
ISBN = {1613-0073},
YEAR = {2008},
PAGES = {11pages},
ABSTRACT = {In this paper we show that subsumption problems in many
lightweight description logics (including ${\cal EL}$)
can be expressed as uniform word problems in classes of
semilattices with monotone operators.
We use possibilities of efficient local reasoning in such
classes of algebras to obtain uniform PTIME decision
procedures for CBox subsumption in ${\cal EL}$ and
extensions thereof. These locality considerations allow
us to present a new family of logics which extend
${\cal EL}$ and also a new extension of ${\cal EL}^+$.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-dualities1999,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Vaz de Carvalho, J{\'u}lia and Ferreirim, Isabel},
TITLE = {Priestley representation for distributive lattices with operators and applications to automated theorem proving},
BOOKTITLE = {Dualities, Interpretability and Ordered Structures},
TYPE = {Extended Abstract},
PADDRESS = {Lisbon},
ADDRESS = {Lisbon, Portugal},
PUBLISHER = {Centro de 'Algebra da Universidade de Lisboa},
YEAR = {1999},
PAGES = {43--54},
ABSTRACT = {We present an extension of the Priestley representation theorem to distributive
lattices with operators.
We then point out how it can be used for automated theorem proving in certain
finitely-valued logics.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-esslli09,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Reasoning in Complex Theories and Applications. Advanced Lecture},
BOOKTITLE = {ESSLLI 2009 : European Summer School in Logic, Language and Information},
PADDRESS = {s.l.},
ADDRESS = {Bordeaux, France},
PUBLISHER = {ESSLLI},
YEAR = {2009},
PAGES = {1--64},
}
@INPROCEEDINGS{Sofronie-Stokkermans-frocos-07,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Konev, Boris and Wolter, Frank},
TITLE = {Hierarchical and modular reasoning in complex theories: The case of local theory extensions},
BOOKTITLE = {Frontiers of Combining Systems. 6th International Symposium FroCos 2007, Proceedings},
PADDRESS = {New York},
ADDRESS = {Liverpool, UK},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4720},
ISBN = {978-3-540-74620-1},
DOI = {10.1007/978-3-540-74621-8_3},
YEAR = {2007},
PAGES = {47--71},
NOTE = {Invited paper},
ABSTRACT = {Many problems in computer science can be reduced to proving the satisfiability
of conjunctions of literals w.r.t. a background theory. This theory can be a
concrete theory (e.g. the theory of real or rational numbers), the extension of
a theory with additional functions (free, monotone, or recursively defined) or
a combination of theories. It is therefore very important to have efficient
procedures for checking the satisfiability of conjunctions of ground literals
in such theories.
We here give an overview of results on hierarchical and modular reasoning in
complex theories. We show that for a special type of extensions of a base
theory, which we call local, hierarchic reasoning is possible (i.e. proof tasks
in the extension can be hierarchically reduced to proof tasks w.r.t. the base
theory). Many theories important for computer science or mathematics fall into
this class (typical examples are theories of data structures, theories of free
or monotone functions, but also functions occurring in mathematical analysis).
In fact, it is often necessary to consider complex extensions, in which various
types of functions or data structures need to be taken into account at the same
time. We show how such local theory extensions can be identified and under
which conditions locality is preserved when combining theories, and we
investigate possibilities of efficient modular reasoning in such theory
combinations.
We present several examples of application domains where such theories occur in
a natural way. We show, in particular, that various phenomena analyzed in the
verification literature can be explained in a unified way using the notion of
locality.},
}
@PROCEEDINGS{Sofronie-Stokkermans-frocos-2011,
EDITOR = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica},
TITLE = {Frontiers of Combining Systems},
PADDRESS = {Heidelberg},
ADDRESS = {Saarbr{\"u}cken, Germany},
PUBLISHER = {Springer},
MONTH = {October},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6989},
ISBN = {978-3-642-24363-9},
YEAR = {2011},
PAGES = {1--275},
}
@INPROCEEDINGS{Sofronie-Stokkermans-frocos2013,
AUTHOR = {Horbach, Matthias and Sofronie-Stokkermans, Viorica},
EDITOR = {Fontaine, Pascal and Ringeissen, Christophe and Schmidt, Renate A.},
TITLE = {Obtaining Finite Local Theory Axiomatizations via Saturation},
BOOKTITLE = {Frontiers of Combining Systems - 9th International Symposium},
PADDRESS = {Heidelberg},
ADDRESS = {Nancy, France},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {8152},
YEAR = {2013},
PAGES = {198--213},
ABSTRACT = {In this paper we present a method for obtaining local sets of clauses from
possibly non-local ones. For this, we follow the work of Basin and Ganzinger
and use saturation under a version of ordered resolution. In order to address
the fact that saturation can generate infinite sets of clauses, we use
constrained clauses and show that a link can be established
between saturation and locality also for constrained clauses:
This often allows us to give a finite representation
of possibly infinite saturated sets of clauses. },
}
@INPROCEEDINGS{Sofronie-Stokkermans-ftp07-abstract,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Ranise, Silvio},
TITLE = {Hierarchical and modular reasoning in complex theories: The case of local theory extensions.},
BOOKTITLE = {Proceedings of the Sixth International Workshop on First-Order Theorem Proving (FTP 2007)},
TYPE = {Abstract},
PADDRESS = {Liverpool, UK},
ADDRESS = {Liverpool, UK},
PUBLISHER = {University of Liverpool},
SERIES = {Technical Report, Department of Computer Science, University of Liverpool.},
VOLUME = {ULCS-07-018},
YEAR = {2007},
PAGES = {1},
NOTE = {the full paper appeared in the proceedings of FroCos 2007},
ABSTRACT = {Many problems in computer science can be reduced to proving the satisfiability
of conjunctions of literals w.r.t. a background theory. This theory can be a
concrete theory (e.g. the theory of real or rational numbers), the extension of
a theory with additional functions (free, monotone, or recursively defined) or
a combination of theories. It is therefore very important to have efficient
procedures for checking the satisfiability of conjunctions of ground literals
in such theories.
We here give an overview of results on hierarchical and modular reasoning in
complex theories. We show that for a special type of extensions of a base
theory, which we call local, hierarchic reasoning is possible (i.e. proof tasks
in the extension can be hierarchically reduced to proof tasks w.r.t. the base
theory). Many theories important for computer science or mathematics fall into
this class (typical examples are theories of data structures, theories of free
or monotone functions, but also functions occurring in mathematical analysis).
In fact, it is often necessary to consider complex extensions, in which various
types of functions or data structures need to be taken into account at the same
time. We show how such local theory extensions can be identified and under
which conditions locality is preserved when combining theories, and we
investigate possibilities of efficient modular reasoning in such theory
combinations.
We present several examples of application domains where such theories occur in
a natural way. We show, in particular, that various phenomena analyzed in the
verification literature can be explained in a unified way using the notion of
locality.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-ftp2000,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Resolution-based theorem proving for {SHn-logics}},
BOOKTITLE = {Automated Deduction in Classical and Non-Classical Logic (Selected Papers of FTP'98)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Vienna, Austria},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1761},
ISBN = {3-540-67190-0},
YEAR = {2000},
PAGES = {268--282},
NOTE = {%Extended version of [Sofronie1998b]. },
ABSTRACT = {In this paper we illustrate by means of an example, namely $SHn$-logics,
a method for translation to clause form and automated theorem proving for
first-order many-valued logics based on distributive lattices with operators.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-getco-06,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Sheaves and geometric logic in concurrency},
BOOKTITLE = {Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006)},
PADDRESS = {-},
ADDRESS = {Bonn, Germany},
PUBLISHER = {-},
MONTH = {August},
YEAR = {2006},
ABSTRACT = {In this paper we present an overview of results that show that
states, transitions and behavior of concurrent systems
can often be modeled as sheaves over a suitable topological space.
In such contexts, geometric logic can be used to test whether
(and describe which) local properties, of individual systems,
are preserved, at a global level, when interconnecting the systems.},
}
@PHDTHESIS{Sofronie-Stokkermans-hab04,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Algebraic and logical methods in automated theorem proving and in the study of concurrency},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Habilitation thesis},
MONTH = {November},
YEAR = {2004},
NOTE = {cumulative habilitation, no publication.},
ABSTRACT = {Vorstellungsvortrag
-------------------
Abstract:
The applications of algebra and logic in computer science are
particularly abundant nowadays; in fact logic is often called
"the calculus of computer science". On the other hand, the
development of computer science has a strong impact on the
research in algebra and logic, and in particular on the research
in computational mathematics and automated theorem proving.
\smallskip
In this talk I will present two, strongly interrelated, directions
of my recent research, which reflect some of the links between
algebra, logic and computer science emphasized above:
\begin{itemize}
\item Decompositions of algebraic structures in terms of simpler
structures, and applications to automated theorem proving.
\item A study of interaction in complex systems, and applications
to modular checking of certain properties of systems obtained
by composing simpler systems.
\end{itemize}
Antrittsvorlesung
-----------------
Abstract:
One of the most important problems in computer science is to
identify decidable and tractable fragments of (first- or
higher-order) logic, and to develop efficient deductive
calculi for these fragments.
However, in most real-life applications it is necessary to
consider combinations of theories which are, usually,
extensions of a shared base theory.
Two important questions arise in this context:
\begin{itemize}
\item Assume that we have a complete prover for a logical theory.
Can one use this prover as a ``black-box'' to prove theorems
in an extension of the theory?
\item Assume that we have complete provers for two theories.
Can we obtain a complete prover for their combination,
by using the provers of the components as ``black-boxes''?
\end{itemize}
In this talk we present several situations in which hierarchical
and modular reasoning is possible, and point out similarities
and differences between various approaches to modular theorem
proving in combinations of logical theories.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-ismvl-2004,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras},
BOOKTITLE = {Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL-2004)},
ORGANIZATION = {IEEE},
PADDRESS = {Los Alamitos, USA},
ADDRESS = {Toronto, Canada},
PUBLISHER = {IEEE Computer Society},
YEAR = {2004},
PAGES = {32--37},
ABSTRACT = {In this paper we give resolution-based decision procedures for
the positive theory of certain finitely-generated varieties of
algebras. The method is based on the existence of
representation theorems for such classes of algebras.},
}
@ARTICLE{Sofronie-Stokkermans-jahrbuch-2006,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {MPG Jahrbuch},
TITLE = {{Automatisches Beweisen in komplexen Theorien}},
YEAR = {2006},
ABSTRACT = {Wir erforschen Rahmenbedingungen, die es erm{\"o}glichen, Beweisaufgaben in
komplexen Theorien modular in Beweisaufgaben f{\"u}r die einfacheren Bestandteile
dieser Theorien zu zerlegen. Durch Ausnutzung der Modularit{\"a}t sind solche
Beweisverfahren besonders flexibel und effizient und deshalb in vielen
Bereichen (wie etwa in der Verifikation komplexer Systeme, aber auch in der
Mathematik oder Wissensrepr{\"a}sentation) anwendbar.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-jim-2003,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Nadif, Mohamed and Napoli, Amedeo and SanJuan, Eric and Sigayret, Alain},
TITLE = {Automated theorem proving by resolution in non-classical logics},
BOOKTITLE = {Fourth International Conference Journees de l'Informatique Messine: Knowledge Discovery and Discrete Mathematics (JIM-03)},
PADDRESS = {Rocquencourt, France},
ADDRESS = {Metz, France},
PUBLISHER = {INRIA},
ISBN = {2-7261-1256-0},
YEAR = {2003},
PAGES = {151--167},
NOTE = {Invited paper},
ABSTRACT = {We present several classes of non-classical logics
(many of which are practically relevant in knowledge
representation)
which can be translated into tractable and relatively
simple fragments of classical logic.
In this context, refinements of resolution can be often
used successfully for automated theorem proving, and
in many cases yield optimal decision procedures.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-ki2008,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Berns, Karsten and Breuel, Thomas},
TITLE = {Efficient hierarchical reasoning about functions over numerical domains},
BOOKTITLE = { KI 2008: Advances in Artificial Intelligence},
PADDRESS = {-},
ADDRESS = {Kaiserslautern, Germany},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {5243},
ISBN = {978-3-540-85844-7},
YEAR = {2008},
PAGES = {135--143},
ABSTRACT = {We show that many properties studied in mathematical analysis
(e.g.\ monotonicity, boundedness, inverse or Lipschitz
properties, possibly combined with continuity and/or
derivability) are expressible as axioms in a class for which
sound and complete hierarchical proof methods for testing
satisfiability of ground formulae exist.
The results are useful for automated reasoning in analysis, and
in the verification of hybrid systems.},
}
@ARTICLE{Sofronie-Stokkermans-lmcs-2008,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {Logical Methods in Computer Science},
TITLE = {Interpolation in local theory extensions},
NUMBER = {4},
MONTH = {October},
VOLUME = {4},
ISBN = {1860-5974},
DOI = {10.2168/LMCS-4(4:1)2008},
YEAR = {2008},
PAGES = {31 pages},
NOTE = {Special issue of LMCS dedicated to IJCAR 2006.},
ABSTRACT = {In this paper we study interpolation in local extensions of a base theory. We
identify situations in which it is possible to obtain interpolants in a
hierarchical manner, by using a prover and a procedure for generating
interpolants in the base theory as black-boxes. We present several examples of
theory extensions in which interpolants can be computed this way, and discuss
applications in verification, knowledge representation, and modular reasoning
in combinations of local theories.},
}
@INCOLLECTION{Sofronie-Stokkermans-moisil-08,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Iorgulescu, Afrodita and Marcus, Solomon and Rudeanu, Sergiu and Vaida, Dragos},
TITLE = {Algebraic and logical methods in computer science: some aspects},
BOOKTITLE = {Grigore C. Moisil and his followers},
ADDRESS = {Bucharest, Romania},
PUBLISHER = {Editura Academiei Romane},
ISBN = {978-973-27-1607-6},
YEAR = {2007},
PAGES = {488--493},
}
@INCOLLECTION{Sofronie-Stokkermans-mvl-2003,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Fitting, Melvin and Orlowska, Ewa},
TITLE = {Representation Theorems and the Semantics of Non-classical Logics, and Applications to Automated Theorem Proving},
BOOKTITLE = {Beyond Two: Theory and Applications of Multiple Valued Logic},
CHAPTER = {3},
ADDRESS = {Berlin, Germany},
PUBLISHER = {Springer},
MONTH = {January},
SERIES = {Studies in Fuzziness and Soft Computing},
VOLUME = {114},
ISBN = {3-7908-1541-1},
YEAR = {2003},
PAGES = {59--100},
ABSTRACT = {We give a uniform presentation of representation and
decidability results related to the Kripke-style
semantics of several non-classical logics.
We show that a general representation theorem
(which has as particular instances the representation
theorems as algebras of sets for Boolean algebras,
distributive lattices and semilattices)
extends in a natural way to several classes of operators
and allows to establish a relationship between algebraic
and Kripke-style models. We illustrate the ideas on several examples.
We conclude by showing how the Kripke-style models thus obtained can be used
(if first-order axiomatizable) for automated theorem proving by
resolution for some non-classical logics.},
}
@ARTICLE{Sofronie-Stokkermans-sacs2013,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {Scientific Annals of Computer Science},
TITLE = {Locality and Applications to Subsumption Testing in EL and Some of its Extensions},
NUMBER = {2},
VOLUME = {23},
YEAR = {2013},
PAGES = {251--284},
ABSTRACT = {n this paper we show that subsumption problems in the description logics
{{mathcal|EL}} and EL+ can be expressed as uniform word problems in classes of
semilattices with monotone operators. We use possibilities of e ficient local
reasoning in such classes of algebras, to obtain uniform PTIME decision
procedures for TBox and CBox subsumption in EL and EL+. These locality
considerations allow us to present a new family of (possibly many-sorted)
logics which extend EL and EL+ with n-ary roles and/or numerical domains.},
}
@INPROCEEDINGS{Sofronie-Stokkermans-tableaux-2002,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Egly, Uwe and Ferm{\"u}ller, Christian},
TITLE = {On uniform word problems involving bridging operators on distributive lattices},
BOOKTITLE = {Automated Reasoning with Analytic and Related Methods : International Conference, TABLEAUX 2002},
PADDRESS = {Berlin, Germany},
ADDRESS = {Copenhagen, Denmark},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {2381},
ISBN = {3-540-43929-3},
YEAR = {2002},
PAGES = {235--250},
ABSTRACT = {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.},
}
@MISC{Sofronie-Stokkermans-tutorial-ki08,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Reasoning in Complex Theories and Applications},
HOWPUBLISHED = {KI 2008: Proceedings of the tutorial "Reasoning in Complex Theories and Applications"},
MONTH = {September},
YEAR = {2008},
PAGES = {64 pages},
ABSTRACT = {One of the most important objectives of the research in mathematics and
computer science is to obtain means of reasoning in and about complex systems.
These can be, for instance complex mathematical theories; programs, or
generally reactive or hybrid systems; distributed databases; or complex systems
in general (e.g. multi-agent systems or reactive or hybrid systems with
embedded software, whose behavior is controlled by databases, reasoning about
knowledge and belief, planning mechanisms, or programs). Proving that such
systems have certain properties (e.g. that they are safe, that they behave
correctly, or that the information they use does not contain inconsistencies)
is extremely important: In safety-critical systems (such as cars, trains,
planes, or power-plants) even small mistakes can provoke disasters. Since the
amount of data which has to be handled in verification tasks is usually huge,
computer support is indispensable. The dream of the scientists is to provide
such correctness proofs automatically. This goal cannot be reached in its full
generality: As shown by undecidability results going back to the work of G{\"o}del,
Church and Turing, it is impossible to write a program for checking arbitrary
properties of general systems. However, for concrete application domains,
automatic procedures exist. It is therefore very important to identify
situations in which automated verification of complex systems is possible. For
this, it is essential to identify theories which are decidable, preferably with
low complexity, and - since concrete problems often are quite heterogeneous in
nature - to obtain methods for efficiently combining decision procedures.
The goal of the tutorial is to give a comprehensive, in-depth perspective of
recent advances in the field of reasoning in complex logical theories, and to
present applications of these results in various areas ranging from formal
verification to reasoning about knowledge. The tutorial introduces the general
principles underlying reasoning in complex theories from a unifying
perspective, gives a survey of recent achievements in the field, and
illustrates the problems and their solutions using a selection of examples from
mathematics, verification, and knowledge representation.},
}
@ARTICLE{Sofronie-Stokkermans-unif-05,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {ACM Transactions on Computational Logic},
TITLE = {On unification for bounded distributive lattices},
NUMBER = {2},
PUBLISHER = {ACM},
MONTH = {April},
VOLUME = {8},
ISBN = {1529-3785},
DOI = {10.1145/1227839.1227844},
YEAR = {2007},
PAGES = {12.1--12.28},
ABSTRACT = {We give a method for deciding unifiability in the variety
of bounded distributive lattices.
For this, we reduce the problem of deciding whether a
unification problem ${\cal S}$ has a solution to the
problem of checking the satisfiability of a set
$\Phi_{\cal S}$ of ground clauses.
This is achieved by using a structure-preserving
translation to clause form.
The satisfiability check can then be performed
either by a resolution-based theorem prover or
by a SAT checker. We apply the method to
unification with free constants and to unification
with linear constant restrictions, and show that,
in fact, it yields a decision procedure for the positive
theory of the variety of bounded distributive lattices.
We also consider the problem of unification over
(i.e.\ in an algebraic extension of) the free lattice.
Complexity issues are also addressed.},
}
@ARTICLE{Sofronie-Stokkermans1999,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {Multiple-Valued Logic - An International Journal},
TITLE = {Automated Theorem Proving by Resolution for Finitely-Valued Logics Based on Distributive Lattices with Operators},
ADDRESS = {Amsterdam, the Netherlands},
NUMBER = {3/4},
PUBLISHER = {Gordon and Breach},
MONTH = {March},
VOLUME = {6},
ISBN = {1023-6627},
YEAR = {2001},
PAGES = {289--344},
NOTE = { },
ABSTRACT = {In this paper we present a method for automated theorem proving in
finitely-valued logics whose algebra of truth values is a distributive lattice
with operators. The method uses the Priestley dual of the algebra of truth
values instead of the algebra itself (this dual
is used as a finite set of possible worlds).
We first present a procedure that constructs, for every formula $\phi$ in the
language of such a logic, a set $\Phi$ of clauses such that $\phi$ is a
theorem if and only if $\Phi$ is unsatisfiable. Compared to related approaches,
the method presented here leads in many cases to a reduction of the number of
clauses that are generated, especially when the set of truth values is not
linearly ordered.
We then discuss several possibilities for checking the unsatisfiability of
$\Phi$, among which a version of signed hyperresolution, and give several
examples. },
}
@INPROCEEDINGS{Sofronie-Stokkermans1999-cade,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Ganzinger, Harald},
TITLE = {On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results},
BOOKTITLE = {Proceedings of the 16th International Conference on Automated Deduction (CADE-16)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Trento, Italy},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1632},
YEAR = {1999},
PAGES = {157--171},
ABSTRACT = {In this paper we give a method for automated theorem proving in the universal
theory of certain varieties of distributive lattices with well-behaved
operators. For this purpose, we use extensions of Priestley's representation
theorem for distributive lattices. We first establish a link between
satisfiability of universal sentences with respect to varieties of distributive
lattices with operators and satisfiability with respect to certain classes of
relational structures. We then use these results for giving a method for
translation to clause form of universal sentences in such varieties, and obtain
decidability and complexity results for the universal theory of some such
varieties. The advantage is that we avoid the explicit use of the full
algebraic structure of such lattices, instead using sets endowed with a
reflexive and transitive relation and with additional functions and relations.
We first studied this type of relationships in the context of finitely-valued
logics and then extended the ideas to more
general non-classical logics. This paper shows that the idea is much more
general. In particular, the method presented here subsumes both existing
methods for translating modal logics to classical logic and methods for
automated theorem proving in finitely-valued logics based on distributive
lattices with operators. },
}
@INPROCEEDINGS{Sofronie-Stokkermans1999-fct,
AUTHOR = {Sofronie-Stokkermans, Viorica and Stokkermans, Karel},
EDITOR = {Ciobanu, Gabriel and Paun, Gheorghe},
TITLE = {Modeling Interaction by Sheaves and Geometric Logic},
BOOKTITLE = {Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Iasi, Romania},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1684},
ISBN = {3-540-66412-2},
YEAR = {1999},
PAGES = {512--523},
ABSTRACT = {In this paper we show that, given a family of interacting systems, many notions
which are important for expressing properties of systems can be modeled as
sheaves over a suitable topological space.
In such contexts, geometric logic can be used to test whether ``local''
properties can be lifted to a global level.
We develop a way to use this method in the study of interacting systems,
illustrated by examples.},
}
@INPROCEEDINGS{Sofronie-Stokkermans1999-ismvl,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Representation Theorems and Automated Theorem Proving in Non-Classical Logics},
BOOKTITLE = {Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic (ISMVL-99)},
ORGANIZATION = {IEEE Computer Society},
PADDRESS = {Los Alamitos, USA},
ADDRESS = {Freiburg im Breisgau, Germany},
PUBLISHER = {IEEE},
MONTH = {May},
ISBN = {0-7695-0161-3},
YEAR = {1999},
PAGES = {242--247},
ABSTRACT = {In this paper we present a method for automated theorem proving in
non-classical logics having as algebraic models bounded distributive lattices
with certain types of operators.
The idea is to use results from Priestley duality for distributive lattices
with operators in order to define a class of Kripke-style models with respect
to which the logic is sound and complete. If this class of Kripke-style models
is elementary, it can then be used for a translation to clause form;
satisfiability of the resulting clauses can be checked by resolution. We
illustrate the general ideas by several examples, one of which is presented in
detail.},
}
@INPROCEEDINGS{Sofronie-Stokkermans1999-lmps,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Cachro, Jacek and Kijania-Placek, Katarzyna},
TITLE = {Resolution-based theorem proving for non-classical logics based on distributive lattices with operators},
BOOKTITLE = {Proceedings of the 11th International Congress of Logic, Methodology and Philosophy of Science. Volume of abstracts},
TYPE = {Abstract},
PADDRESS = {Cracow, Poland},
ADDRESS = {Cracow, Poland},
PUBLISHER = {The Faculty of Philosophy, Jagellonian University},
MONTH = {August},
ISBN = {83-912252-0-8},
YEAR = {1999},
PAGES = {481--481},
}
@INCOLLECTION{Sofronie-Stokkermans2000-atlas-1,
AUTHOR = {Iturrioz, Luisa and Sofronie-Stokkermans, Viorica},
EDITOR = {Iturrioz, Luisa and Orlowska, Ewa and Turunen, Esko},
TITLE = {{SHn-algebras} ({Symmetric} {Heyting} algebras of order n)},
BOOKTITLE = {COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures},
TYPE = {Technical Report},
ADDRESS = {Tampere},
NUMBER = {75},
PUBLISHER = {Tampere University of Technology (Mathematics)},
MONTH = {January},
SERIES = {Department of Information Technology. Mathematics Report},
ISBN = {952-150-386-6},
YEAR = {2000},
PAGES = {1--11},
}
@INCOLLECTION{Sofronie-Stokkermans2000-atlas-2,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Iturrioz, Luisa and Orlowska, Ewa and Turunen, Esko},
TITLE = {Some properties of {Kleene} algebras},
BOOKTITLE = {COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures},
TYPE = {Technical Report},
ADDRESS = {Tampere},
NUMBER = {75},
PUBLISHER = {Tampere University of Technology (Mathematics)},
MONTH = {January},
SERIES = {Department of Information Technology. Mathematics Report},
ISBN = {952-150-386-6},
YEAR = {2000},
PAGES = {1--7},
}
@INPROCEEDINGS{Sofronie-Stokkermans2001-ismvl,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Representation theorems and the semantics of (semi)lattice-based logics},
BOOKTITLE = {Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logics},
ORGANIZATION = {IEEE Computer Society, Institute of Computer Science Polish Academy of Sciences},
PADDRESS = {Los Alamitos, USA},
ADDRESS = {Warsaw, Poland},
PUBLISHER = {IEEE},
ISBN = {0-7695-1083-3},
YEAR = {2001},
PAGES = {125--134},
NOTE = { },
ABSTRACT = {This paper gives a unified presentation of various non-classical
logics. We show that a general representation theorem (which has
as particular instances the representation theorems as algebras
of sets for Boolean algebras, distributive lattices and
semilattices) allows to establish a relationship between
algebraic models and Kripke-style models, and illustrate the
ideas on several examples.
Based on this, we present a method for automated theorem
proving by resolution in such logics.
Other representation theorems, as algebras of sets or as
algebras of relations, as well as relational models are
also mentioned. },
}
@INPROCEEDINGS{Sofronie-Stokkermans2006,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Contejean, Evelyne},
TITLE = {On unification in certain finitely generated varieties of algebras},
BOOKTITLE = {Proceedings of the 21th International Workshop on Unification (UNIF 2007)},
PADDRESS = {-},
ADDRESS = {Paris, France},
YEAR = {2007},
PAGES = {1--5},
}
@PROCEEDINGS{Sofronie-Stokkermans2009-addct-unif,
EDITOR = {Lynch, Christopher and Narendran, Paliath and Baader, Franz and Ghilardi, Silvio and Hermann, Miki and Sofronie-Stokkermans, Viorica and Tiwari, Ashish},
TITLE = {UNIF 2009, 23nd International Workshop on Unification and ADDCT 2009
Automated Deduction: Decidability, Complexity, Tractability : proceedings},
PADDRESS = {Montreal, Canada},
ADDRESS = {McGill University, Montreal, Canada},
PUBLISHER = {McGill University},
YEAR = {2009},
PAGES = {1--87},
}
@ARTICLE{Sofronie-Stokkermans2009-jsc-addct,
AUTHOR = {Ghilardi, Silvio and Sattler, Ulrike and Sofronie-Stokkermans, Viorica and Tiwari, Ashish},
JOURNAL = {Journal of Symbolic Computation},
TITLE = {Special issue on automated deduction: Decidability, complexity, tractability},
ADDRESS = {Amsterdam},
NUMBER = {2},
PUBLISHER = {Elsevier},
VOLUME = {45},
ISBN = {0747-7171},
DOI = {10.1016/j.jsc.2009.05.006},
YEAR = {2010},
PAGES = {151--152},
}
@INPROCEEDINGS{Sofronie-Stokkermans2010-ijcar,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Giesl, J{\"u}rgen and H{\"a}hnle, Reiner},
TITLE = {Hierarchical Reasoning for the Verification of Parametric Systems},
BOOKTITLE = {Automated Reasoning : 5th International Joint Conference, IJCAR 2010},
PADDRESS = {Berlin},
ADDRESS = {Edinburgh},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6173},
ISBN = {978-3-642-14202-4},
DOI = {10.1007/978-3-642-14203-1_15},
YEAR = {2010},
PAGES = {171--187},
ABSTRACT = {We study certain classes of verification problems for parametric
reactive and hybrid systems, and identify the types of logical
theories which can be used for modeling such systems and the
reasoning tasks which need to be solved in this context.
We identify properties of the underlying theories which ensure
that these classes of verification problems can be solved
efficiently, give examples of theories with the desired
properties, and illustrate the methods we use on several
examples.},
}
@ARTICLE{Sofronie-Stokkermans2012-jsc-ftp,
AUTHOR = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
JOURNAL = {Journal of Symbolic Computation},
TITLE = {First-order theorem proving: Foreword},
ADDRESS = {Amsterdam},
NUMBER = {9},
PUBLISHER = {Elsevier},
MONTH = {September},
VOLUME = {47},
ISBN = {0747-7171},
DOI = {10.1016/j.jsc.2011.12.030},
YEAR = {2012},
PAGES = {1009--1010},
}
@ARTICLE{Sofronie-Stokkermans2013-jar-cade-special-issue,
AUTHOR = {Bjorner, Nikolaj and Sofronie-Stokkermans, Viorica},
JOURNAL = {Journal of Automated Reasoning},
TITLE = {Preface: Special Issue of Selected Extended Papers of CADE-23},
NUMBER = {1},
PUBLISHER = {Springer},
VOLUME = {51},
ISBN = {0168-7433},
YEAR = {2013},
PAGES = {1--2},
}
@INPROCEEDINGS{Sofronie-verify-06,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Autexier, Serge and Mantel, Heiko},
TITLE = {Local reasoning in verification},
BOOKTITLE = {IJCAR'06 Workshop : VERIFY'06: Verification Workshop},
PADDRESS = {-},
ADDRESS = {Seattle, USA},
PUBLISHER = {-},
MONTH = {August},
YEAR = {2006},
PAGES = {128--145},
ABSTRACT = {The goal of this paper is to illustrate the wide applicability
in verification of results on local reasoning, and especially
on hierarchical reasoning in local theory extensions.
The paper contains a survey of our results on reasoning in
local theory extensions, ranging from characterizations of
locality to interpolation. In addition, several examples are
provided, emphasizing theories occurring in a natural way in
verification. We give several examples -- some already
existing in the literature, others obtained during the work
in the AVACS project -- of application domains where such
theories occur in a natural way.},
}
@INCOLLECTION{Sofronie-wlphg11,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Voronkov, Andrei and Weidenbach, Christoph},
TITLE = {On combinations of local theory extensions},
BOOKTITLE = {Programming Logics, Essays in Memory of Harald Ganzinger},
ADDRESS = {Berlin},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7797},
ISBN = {978-3-642-37650-4},
YEAR = {2013},
PAGES = {392--413},
ABSTRACT = {Many problems in mathematics and computer science can be
reduced to proving the satisfiability of conjunctions of
literals in a background theory which is often the extension
of a base theory with additional functions or a combination
of theories.
It is therefore important to have efficient procedures for
checking satisfiability of conjunctions of ground literals
in extensions and combinations of theories.
For a special type of theory extensions, namely {\em local
extensions}, hierarchic reasoning, in which a theorem prover
for the base theory can be used as a ``black box'',
is possible. Many theories used in computer science or
mathematics are local extensions of a base theory.
However, often it is necessary to consider complex extensions
of a theory, with various types of functions.
In this paper we identify situations in which
a combination of local extensions of a base theory
is guaranteed to be again a local extension of the base theory.
We thus obtain criteria both for recognizing wider classes of
local theory extensions, and for modular reasoning in
combinations of theories over non-disjoint signatures.},
}
@ARTICLE{Sofronie1997a,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {Multiple-Valued Logic - An International Journal},
TITLE = {Priestley Duality for {SHn-algebras} and Applications to the Study of {Kripke-style} Models for {SHn-logics}},
ADDRESS = {Amsterdam, the Netherlands},
NUMBER = {4},
PUBLISHER = {Gordon and Breach},
VOLUME = {5},
ISBN = {1023-6627},
YEAR = {2000},
PAGES = {281--305},
ABSTRACT = {The main goal of this paper is to show that the Priestley duality for
SHn-algebras can help to establish a link between the algebraic and
Kripke-style semantics for SHn-logics. We present a Priestley duality theorem
for SHn-algebras, and note that the dual space of an SHn-algebra satisfies in
particular the properties of a Kripke model for SHn-logics. We then show that
Priestley duality can help in proving the soundness and completeness of
SHn-logics with respect to the class of SHn-frames in a direct way, by using
only soundness and completeness of SHn-logics with respect to the variety of
SHn-algebras. },
}
@ARTICLE{Sofronie1997b,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {Studia Logica},
TITLE = {Duality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. {Part I}},
ADDRESS = {Dordrecht, the Netherlands},
NUMBER = {1},
PUBLISHER = {Kluwer},
MONTH = {February},
VOLUME = {64},
ISBN = {0039-3215},
YEAR = {2000},
PAGES = {93--132},
ABSTRACT = {The main goal of this paper is to explain the link between the algebraic and
the Kripke-style models for certain classes of propositional logics. We start
by presenting a Priestley-type duality for distributive lattices endowed with
a general class of well-behaved operators.
We then show that finitely-generated varieties of distributive lattices with
operators are closed under canonical embedding algebras.
The results are used in the second part of the paper to construct topological
and non-topological Kripke-style models for logics that are sound and complete
with respect to varieties of distributive lattices with operators in the
above-mentioned classes. },
}
@ARTICLE{Sofronie1997c,
AUTHOR = {Sofronie-Stokkermans, Viorica},
JOURNAL = {Studia Logica},
TITLE = {Duality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. {Part II}},
ADDRESS = {Dordrecht, the Netherlands},
NUMBER = {2},
PUBLISHER = {Kluwer},
MONTH = {March},
VOLUME = {64},
ISBN = {0039-3215},
YEAR = {2000},
PAGES = {151--172},
ABSTRACT = {In this paper we explain the link between the algebraic models and the
Kripke-style models for certain classes of propositional non-classical logics.
We consider logics that are sound and complete with respect to varieties of
distributive lattices with certain classes of well-behaved operators for which
a Priestley-style duality holds, and present a way of constructing topological
and non-topological Kripke-style models for these types of logics.
Moreover, we show that, under certain additional assumptions on the variety of
the algebraic models of the given logics, soundness and completeness with
respect to these classes of Kripke-style models follows by using entirely
algebraical arguments from the soundness and completeness of the logic with
respect to its algebraic models. },
}
@INPROCEEDINGS{Sofronie1998a,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Prade, Henri},
TITLE = {On Translation of Finitely-Valued Logics to Classical First-Order Logic},
BOOKTITLE = {Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98)},
PADDRESS = {Chichester, USA},
ADDRESS = {Brighton, UK},
PUBLISHER = {Wiley},
ISBN = {0-471-98431-0},
YEAR = {1998},
PAGES = {410--411},
ABSTRACT = {The main goal of this paper is to give a better understanding of
existing many-valued resolution procedures, and thus help to improve
the efficiency of automated theorem proving in finitely-valued logics.
First, we briefly present a method for translation to clause form
in finitely-valued logics based on distributive lattices with operators,
which uses the Priestley dual of the algebra of truth values.
We show that the unsatisfiability of the set of signed clauses thus
obtained can be checked by a version of signed negative hyperresolution.
This extends the results established by H\"ahnle in the case of regular logics,
where the set of truth values is linearly ordered. As in the case of regular
hyperresolution, also our version of signed hyperresolution is surprisingly
similar to the classical version. In the second part of the paper we explain
why regular logics and the logics we consider are so well-behaved.
We show that in both cases the translation to clause form is actually a
translation to classical logic, and that soundness and completeness of various
refinements of the (signed) resolution procedure follow as a consequence of
results from first-order logic. Decidability and complexity results for signed
clauses follow as well, by using results from first-order logic. This explains
and extends earlier results on theorem proving in finitely-valued logics.},
}
@TECHREPORT{Sofronie1998b,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Resolution-based Theorem Proving for SHn-Logics},
INSTITUTION = {Technische Universit{\"a}t Wien},
TYPE = {Technical Report},
ADDRESS = {Vienna, Austria},
NUMBER = {E1852-GS-981},
MONTH = {November},
YEAR = {1998},
PAGES = {224--233},
NOTE = {an extended version will appear in LNCS (subseries LNAI); Proceedings of FTP'98},
ABSTRACT = {In this paper we illustrate by means of an example, namely $SHn$-logics,
a method for translation to clause form and automated theorem proving for
first-order many-valued logics based on distributive lattices with operators.},
}
@INPROCEEDINGS{Sofronie1998c,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Eklund, Patrick and Escalada-Imaz, Gonzalo and Haehnle, Reiner and Vojtas, Peter},
TITLE = {Representation Theorems and Automated Theorem Proving in Certain Classes of Non-Classical Logics},
BOOKTITLE = {Proceedings of the Workshop on Many-Valued Logic for AI Applications (ECAI-98)},
PADDRESS = {Brighton, UK},
ADDRESS = {Brighton, UK},
PUBLISHER = {ECAI},
MONTH = {August},
YEAR = {1998},
ABSTRACT = {The main goal of this paper is to present a method for translation to clause
form in finitely-valued logics having as algebras of truth values distributive
lattices with certain types of operators. The method uses the Priestley dual of
the algebra of truth values. We illustrate these general ideas by several
examples, and show that the general complexity can be further improved by using
the structure of particular algebras of truth values. We then show that these
ideas are actually much more general: we further develop one of our previous
ideas where we showed that Priestley duality is useful in better understanding
the link between algebraic and Kripke-style models for certain non-classical
logics, and give several examples.},
}
@INPROCEEDINGS{SturmTiwari:11a,
AUTHOR = {Sturm, Thomas and Tiwari, Ashish},
EDITOR = {Leykin, Anton},
TITLE = {Verification and Synthesis Using Real Quantifier Elimination},
BOOKTITLE = {ISSAC 2011 : Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation},
ORGANIZATION = {Association for Computing Machinery (ACM)},
PADDRESS = {New York, NY},
ADDRESS = {San Jose, CA},
PUBLISHER = {ACM},
MONTH = {June},
ISBN = {978-1-4503-0675-1},
DOI = {10.1145/1993886.1993935},
YEAR = {2011},
PAGES = {329--336},
ABSTRACT = {We present the application of real quantifier elimination to formal
verification and synthesis of continuous and switched dynamical systems.
Through a series of case studies, we show how first-order formulas over the
reals arise when formally analyzing models of complex control systems. Existing
off-the-shelf quantifier elimination procedures are not successful in
eliminating quantifiers from many of our benchmarks. We therefore automatically
combine three established software components: virtual subtitution based
quantifier elimination in Reduce/Redlog, cylindrical algebraic decomposition
implemented in Qepcad, and the simplifier Slfq implemented on top of Qepcad. We
use this combination to successfully analyze various models of systems
including adaptive cruise control in automobiles, adaptive flight control
system, and the classical inverted pendulum problem studied in control theory.},
}
@PROCEEDINGS{SturmZengler2011,
EDITOR = {Sturm, Thomas and Zengler, Christoph},
TITLE = {Automated Deduction in Geometry : 7th International Workshop, ADG 2008},
PADDRESS = {Berlin},
ADDRESS = {Shanghai, China},
PUBLISHER = {Springer},
MONTH = {May},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6301},
ISBN = {978-3-642-21045-7},
DOI = {10.1007/978-3-642-21046-4},
YEAR = {2011},
PAGES = {1--225},
}
@TECHREPORT{Suda2010,
AUTHOR = {Suda, Martin and Weidenbach, Christoph and Wischnewski, Patrick},
TITLE = {On the Saturation of YAGO},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
TYPE = {Research Report},
ADDRESS = {Saarbr{\"u}cken},
NUMBER = {MPI-I-2010-RG1-001},
MONTH = {February},
ISBN = {0946-011X},
YEAR = {2010},
PAGES = {56S.},
}
@INPROCEEDINGS{SudaSutcliffeWischnewskiLamotteKI2009,
AUTHOR = {Suda, Martin and Sutcliffe, Geoff and Wischnewski, Patrick and Lamotte-Schubert, Manuel and de Melo, Gerard},
EDITOR = {Mertsching, B{\"a}rbel and Hund, Marcus and Aziz, Zaheer},
TITLE = {External Sources of Axioms in Automated Theorem Proving},
BOOKTITLE = {KI 2009: Advances in Artificial Intelligence},
PADDRESS = {Berlin, Germany},
ADDRESS = {Paderborn, Germany},
PUBLISHER = {Springer},
MONTH = {September},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {5803},
ISBN = {978-3-642-04616-2},
DOI = {10.1007/978-3-642-04617-9_36},
YEAR = {2009},
PAGES = {281--288},
ABSTRACT = {In recent years there has been a growing demand for Automated
Theorem Proving (ATP) in large theories, which often have more
axioms than can be handled effectively as normal internal axioms. This
work addresses the issues of accessing \emph{external sources of axioms} from a
first-order logic ATP system, and presents an implemented ATP system
that retrieves external axioms asynchronously, on demand.},
}
@INPROCEEDINGS{SudaWeidenbachIJCAR2012,
AUTHOR = {Suda, Martin and Weidenbach, Christoph},
EDITOR = {Gramlich, Bernhard and Miller, Dale and Sattler, Uli},
TITLE = {A {PLTL}-prover based on labelled superposition with partial model guidance},
BOOKTITLE = {Automated Reasoning : 6th International Joint Conference, IJCAR 2012},
PADDRESS = {Berlin},
ADDRESS = {Manchester, UK},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7364},
ISBN = {978-3-642-31364-6},
DOI = {10.1007/978-3-642-31365-3_42},
YEAR = {2012},
PAGES = {537--543},
ABSTRACT = {Labelled superposition (LPSup) is a new calculus for PLTL. One of its
distinguishing features, in comparison to other resolution-based approaches, is
its ability to construct partial models on the fly. We use this feature to
design a new decision procedure for the logic, where the models are effectively
used to guide the search. On a representative set of benchmarks, our
implementation is then shown to considerably advance the state of the art.},
}
@INPROCEEDINGS{SudaWeidenbachLPAR2012,
AUTHOR = {Suda, Martin and Weidenbach, Christoph},
EDITOR = {Bj{\o}rner, Nikolaj and Voronkov, Andrei},
TITLE = {Labelled Superposition for {PLTL}},
BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18},
PADDRESS = {Berlin},
ADDRESS = {M{\'e}rida, Venezuela},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7180},
ISBN = {978-3-642-28716-9},
DOI = {10.1007/978-3-642-28717-6_31},
YEAR = {2012},
PAGES = {391--405},
ABSTRACT = {This paper introduces a new decision procedure for PLTL based on labelled
superposition.
Its main idea is to treat temporal formulas as infinite sets of purely
propositional clauses over an extended signature. These infinite sets are then
represented by finite sets of labelled propositional clauses. The new
representation enables the replacement of the complex temporal resolution
rule, suggested by existing resolution calculi for PLTL, by a fine grained
repetition check of finitely saturated labelled clause sets followed by a
simple inference. The completeness argument is based on the standard model
building idea from superposition. It inherently justifies ordering
restrictions, redundancy elimination and effective partial model building. The
latter can be directly used to effectively generate counterexamples of
non-valid PLTL conjectures out of saturated labelled clause sets in a
straightforward way.},
}
@INPROCEEDINGS{SudaWeidenbachWischnewskiIJCAR10,
AUTHOR = {Suda, Martin and Weidenbach, Christoph and Wischnewski, Patrick},
EDITOR = {Giesl, J{\"u}rgen and H{\"a}hnle, Reiner},
TITLE = {On the Saturation of {YAGO}},
BOOKTITLE = {Automated Reasoning : 5th International Joint Conference, IJCAR 2010},
PADDRESS = {Berlin},
ADDRESS = {Edinburgh, UK},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {6173},
ISBN = {978-3-642-14202-4},
DOI = {10.1007/978-3-642-14203-1_38},
YEAR = {2010},
PAGES = {441--456},
ABSTRACT = {YAGO is an automatically generated ontology out of Wikipedia
and WordNet. It is eventually represented in a proprietary
flat text file format and a core comprises 10 million facts
and formulas. We present a translation of YAGO into the
Bernays-Sch¨onfinkel Horn class with equality. A new
variant of the superposition calculus is sound, complete
and terminating for this class. Together with extended term
indexing data structures the new calculus is implemented in
Spass-YAGO. YAGO can be finitely saturated by Spass-YAGO in
about 1 hour.We have found 49 inconsistencies in the original
generated ontology which we have fixed. Spass-YAGO can then
prove non-trivial conjectures with respect to the resulting
saturated and consistent clause set of about 1.4 GB in less
than one second.},
}
@MASTERSTHESIS{Teucke13,
AUTHOR = {Teucke, Andreas},
TITLE = {CDCL with Reduction},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
MONTH = {May},
YEAR = {2013},
}
@INPROCEEDINGS{tran-atva08,
AUTHOR = {Lynch, Christopher and Tran, Duc-Khanh},
EDITOR = {Cha, Sungdeok (Steve) and Choi, Jin-Young and Kim Moonzoo and Lee, Insup and Viswanathan, Mahesh},
TITLE = {{SMELS}: Satisfiability Modulo Equality with Lazy Superposition},
BOOKTITLE = {Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008},
PADDRESS = {Berlin / Heidelberg},
ADDRESS = {Seoul, Korea},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {5311},
ISBN = {0302-9743},
YEAR = {2008},
PAGES = {186--200},
ABSTRACT = {We give a method for extending efficient SMT solvers to handle quantifiers,
using Superposition inference rules. In our method, the input formula is
converted into CNF as in traditional first order logic theorem provers. The
ground clauses are given to the SMT solver, which runs a DPLL method to build
partial models. The partial model is passed to a Congruence Closure procedure,
as is normally done in SMT. Congruence Closure calculates all reduced
(dis)equations in the partial model and passes them to a Superposition
procedure, along with a justification. The Superposition procedure then
performs an inference rule, which we call Justified Superposition, between the
(dis)equations and the nonground clauses, plus usual Superposition rules with
the nonground clauses. Any resulting ground clauses are provided to the DPLL
engine. We prove the completeness of this method, using a nontrivial
modification of Bachmair and Ganzinger’s model generation technique. We believe
this combination uses the best of both worlds, an SMT process to handle ground
clauses efficiently, and a Superposition procedure which uses orderings to
handle the nonground clauses.},
}
@ARTICLE{tran-decproc-jsc,
AUTHOR = {Tran, Duc-Khanh and Ringeissen, Christopher and Ranise, Silvio and Kirchner, Helene},
JOURNAL = {Journal of Symbolic Computation},
TITLE = {Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation},
ADDRESS = {Amsterdam, The Netherlands},
NUMBER = {2},
PUBLISHER = {Elsevier},
VOLUME = {45-},
ISBN = {0747-7171},
DOI = {10.1016/j.jsc.2008.10.006},
YEAR = {2009},
PAGES = {261--286},
NOTE = {Accepted for publication},
ABSTRACT = {Decision procedures are key components of theorem provers and
constraint satisfaction systems. Their modular combination is of
prime interest for building efficient systems, but their effective
use is often limited by poor interface capabilities, when such
procedures only provide a simple ``sat/unsat'' answer. In this
paper, we develop a framework to design cooperation schemas between
such procedures while maintaining modularity of their
interfaces. First, we use the framework to specify and prove the
correctness of classic combination schemas by Nelson-Oppen and
Shostak. Second, we introduce the concept of deduction complete
satisfiability procedures, we show how to build them for large
classes of theories, then we provide a schema to modularly
combine them. Third, we consider the problem of modularly
constructing explanations for combinations by re-using available
proof-producing procedures for the component theories.},
}
@INPROCEEDINGS{VoronkovetAl13,
AUTHOR = {Kapur, Deepak and Nieuwenhuis, Robert and Voronkov, Andrei and Weidenbach, Christoph and Wilhelm, Reinhard},
EDITOR = {Voronkov, Andrei and Weidenbach, Christoph},
TITLE = {Harald Ganzinger's Legacy: Contributions to Logics and Programming},
BOOKTITLE = {Programming Logics},
PADDRESS = {Heidelberg},
ADDRESS = {Festschrift},
PUBLISHER = {Springer},
YEAR = {2013},
}
@BOOK{VoronkovWeidenbach13,
AUTHOR = {Voronkov, Andrei Voronkov and Weidenbach, Christoph},
TITLE = {Programming Logics - Essays in Memory of Harald Ganzinger},
ADDRESS = {Heidelberg},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7797},
ISBN = {978-3-642-37650-4},
YEAR = {2013},
PAGES = {445},
}
@PHDTHESIS{Waldmann1997,
AUTHOR = {Waldmann, Uwe},
TITLE = {Cancellative Abelian Monoids in Refutational Theorem Proving},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Doctoral dissertation},
MONTH = {July},
YEAR = {1997},
ABSTRACT = {We present a constraint superposition calculus in which the axioms of
cancellative abelian monoids and, optionally, further axioms (e.g.,
torsion-freeness) are integrated. Cancellative abelian monoids comprise abelian
groups, but also such ubiquitous structures as the natural numbers or
multisets. Our calculus requires neither extended clauses nor explicit
inferences with the theory axioms. The number of variable overlaps is
significantly reduced by strong ordering restrictions and powerful variable
elimination techniques; in divisible torsion-free abelian groups, variable
overlaps can even be avoided completely. Thanks to the equivalence of
torsion-free cancellative and totally ordered abelian monoids, our calculus
allows us to solve equational problems in totally ordered abelian monoids
without requiring a detour via ordering literals.},
}
@INPROCEEDINGS{Waldmann1997FTP,
AUTHOR = {Waldmann, Uwe},
EDITOR = {Bonacina, Maria Paola and Furbach, Ulrich},
TITLE = {A Superposition Calculus for Divisible Torsion-Free Abelian Groups},
BOOKTITLE = {Proceedings of the International Workshop on First-Order Theorem Proving (FTP-97)},
TYPE = {Extended Abstract},
PADDRESS = {Linz, Austria},
ADDRESS = {Linz, Austria},
NUMBER = {97-50},
PUBLISHER = {Johannes Kepler Universit{\"a}t},
SERIES = {RISC-Linz Report Series},
YEAR = {1997},
PAGES = {130--134},
ABSTRACT = {Variable overlaps are one of the main sources for the inefficiency of AC or ACU
theorem proving calculi. In the presence of the axioms of abelian groups or at
least cancellative abelian monoids, ordering restrictions allow us to avoid
some of these overlaps, but inferences with unshielded variables remain
necessary. In divisible torsion-free abelian groups, for instance the rational
numbers, every clause can be transformed into an equivalent clause without
unshielded variables. We show how such a variable elimination algorithm can be
integrated into the cancellative superposition calculus. The resulting calculus
is refutationally complete with respect to the axioms of divisible torsion-free
abelian groups and allows us to dispense with variable overlaps altogether. If
abstractions are performed eagerly, the calculus makes it furthermore possible
to avoid the computation of AC unifiers and AC orderings.},
}
@INPROCEEDINGS{Waldmann1998,
AUTHOR = {Waldmann, Uwe},
EDITOR = {Kirchner, Claude and Kirchner, H{\'e}l{\`e}ne},
TITLE = {Superposition for Divisible Torsion-Free Abelian Groups},
BOOKTITLE = {Proceedings of the 15th International Conference on Automated Deduction (CADE-98)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Lindau, Germany},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1421},
ISBN = {3-540-64675-2},
YEAR = {1998},
PAGES = {144--159},
ABSTRACT = {Variable overlaps are one of the main sources for the inefficiency of AC or ACU
theorem proving calculi. In the presence of the axioms of abelian groups or at
least cancellative abelian monoids, ordering restrictions allow us to avoid
some of these overlaps, but inferences with unshielded variables remain
necessary. In divisible torsion-free abelian groups, for instance the rational
numbers, every clause can be transformed into an equivalent clause without
unshielded variables. We show how such a variable elimination algorithm can be
integrated into the cancellative superposition calculus. The resulting calculus
is refutationally complete with respect to the axioms of divisible torsion-free
abelian groups and allows us to dispense with variable overlaps altogether. If
abstractions are performed eagerly, the calculus makes it furthermore possible
to avoid the computation of AC unifiers and AC orderings.},
}
@ARTICLE{Waldmann1998IPL,
AUTHOR = {Waldmann, Uwe},
JOURNAL = {Information Processing Letters},
TITLE = {Extending reduction orderings to {ACU}-compatible reduction orderings},
ADDRESS = {Amsterdam, the Netherlands},
NUMBER = {1},
PUBLISHER = {Elsevier},
MONTH = {July},
VOLUME = {67},
ISBN = {0020-0190},
YEAR = {1998},
PAGES = {43--49},
ABSTRACT = {We show that every reduction ordering over terms not containing $+$ that is
total on ground terms and for which $0$ is minimal can be extended to an
ordering that is ACU-compatible (or AC-compatible) and has the multiset
property.To construct the extension ordering we use a variant of the
self-labelling technique of Middeldorp, Ohsaki, and Zantema.},
}
@INPROCEEDINGS{Waldmann1999LPAR,
AUTHOR = {Waldmann, Uwe},
EDITOR = {Ganzinger, Harald and McAllester, David and Voronkov, Andrei},
TITLE = {Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups},
BOOKTITLE = {Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Tbilisi, Georgia},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1705},
ISBN = {3-540-66492-0},
YEAR = {1999},
PAGES = {131--147},
NOTE = {%Earlier version: Technical Report MPI-I-1999-2-003, Max-Planck-Institut f{\"u}r
Informatik, Saarbr{\"u}cken},
ABSTRACT = {In divisible torsion-free abelian groups, the efficiency of the cancellative
superposition calculus can be greatly increased by combining it with a variable
elimination algorithm that transforms every clause into an equivalent clause
without unshielded variables. We show that the resulting calculus is not only
refutationally complete (even in the presence of arbitrary free function
symbols), but that it is also a decision procedure for the theory of divisible
torsion-free abelian groups.},
}
@INPROCEEDINGS{Waldmann2001IJCAR,
AUTHOR = {Waldmann, Uwe},
EDITOR = {Gor{\'e}, Rajeev and Leitsch, Alexander and Nipkow, Tobias},
TITLE = {Superposition and Chaining for Totally Ordered Divisible Abelian Groups ({Extended} Abstract)},
BOOKTITLE = {Automated reasoning : First International Joint Conference, IJCAR 2001},
PADDRESS = {Berlin, Germany},
ADDRESS = {Siena, Italy},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {2083},
ISBN = {3-540-42254-4},
YEAR = {2001},
PAGES = {226--241},
ABSTRACT = {We present a calculus for first-order theorem proving in the presence of the
axioms of totally ordered divisible abelian groups. The calculus extends
previous superposition or chaining calculi for divisible torsion-free abelian
groups and dense total orderings without endpoints. As its predecessors, it is
refutationally complete and requires neither explicit inferences with the
theory axioms nor variable overlaps. It offers thus an efficient way of
treating equalities and inequalities between additive terms over, e.g., the
rational numbers within a first-order theorem prover.},
}
@ARTICLE{Waldmann2002aJSC,
AUTHOR = {Waldmann, Uwe},
JOURNAL = {Journal of Symbolic Computation},
TITLE = {Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving ({Part I})},
ADDRESS = {Amsterdam, the Netherlands},
NUMBER = {6},
PUBLISHER = {Elsevier},
MONTH = {June},
VOLUME = {33},
ISBN = {0747-7171},
YEAR = {2002},
PAGES = {777--829},
ABSTRACT = {We present superposition calculi in which the axioms
of cancellative abelian monoids and, optionally, the
torsion-freeness axiom are integrated. Cancellative
abelian monoids comprise abelian groups, but also such
ubiquitous structures as the natural numbers or multisets.
Our calculi require neither extended clauses nor explicit
inferences with the theory axioms. Compared with
AC-superposition calculi, the number of variable overlaps
is significantly reduced by strong ordering restrictions. },
}
@ARTICLE{Waldmann2002bJSC,
AUTHOR = {Waldmann, Uwe},
JOURNAL = {Journal of Symbolic Computation},
TITLE = {Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving ({Part II})},
ADDRESS = {Amsterdam, the Netherlands},
NUMBER = {6},
PUBLISHER = {Elsevier},
MONTH = {June},
VOLUME = {33},
ISBN = {0747-7171},
YEAR = {2002},
PAGES = {831--861},
ABSTRACT = {Cancellative superposition is a refutationally complete
calculus for first-order equational theorem proving in the
presence of the axioms of cancellative abelian monoids, and,
optionally, the torsion-freeness axioms. Thanks to strengthened
ordering restrictions, cancellative superposition avoids some
of the inefficiencies of classical AC-superposition calculi.
We show how the efficiency of cancellative superposition can
be further improved by using variable elimination techniques,
leading to a significant reduction of the number of variable
overlaps. In particular, we demonstrate that in divisible
torsion-free abelian groups, variable overlaps, AC-unification
and AC-orderings can be avoided completely.},
}
@INPROCEEDINGS{Waldmann2002IUC,
AUTHOR = {Waldmann, Uwe},
TITLE = {A New Input Technique for Accented Letters in Alphabetical Scripts},
BOOKTITLE = {Proceedings of the 20th International Unicode Conference},
PADDRESS = {Mountain View, CA, USA},
ADDRESS = {Washington, DC, USA},
PUBLISHER = {The Unicode Consortium},
MONTH = {January},
YEAR = {2002},
PAGES = {C12},
ABSTRACT = {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).},
}
@ARTICLE{Waldmann92a,
AUTHOR = {Waldmann, Uwe},
JOURNAL = {Theoretical Computer Science},
TITLE = {Semantics of Order-Sorted Specifications},
NUMBER = {1},
PUBLISHER = {North-Holland Publishing Co.},
VOLUME = {94},
ISBN = {0304-3975},
YEAR = {1992},
PAGES = {1--35},
ABSTRACT = {Order-sorted specifications (i.e., many-sorted specifications with subsort
relations) have been proved to be a useful tool for the description of
partially defined functions and error handling in abstract data types. \par
Several definitions for order-sorted algebras have been proposed. In some
papers an operator symbol, which may be multiply declared, is interpreted by a
family of functions (``overloaded'' algebras), in other papers it is always
interpreted by a single function (``non-overloaded'' algebras). On the one
hand, we try to demonstrate the differences between these two approaches with
respect to equality, rewriting, and completion; on the other hand, we prove
that in fact both theories can be studied parallelly, provided that certain
notions are suitably defined. \par The overloaded approach differs from the
many-sorted and the non-overloaded case, in that the overloaded term algebra is
not necessarily initial. We give a decidable sufficient criterion for the
initiality of the term algebra, which is less restrictive than GJM-regularity
as proposed by Goguen, Jouannaud, and Meseguer. \par Sort decreasingness is an
important property of rewrite system, since it ensures that confluence and
Church-Rosser property are equivalent, that the overloaded and non-overloaded
rewrite relations agree, and that variable overlaps do not yield critical
pairs. We prove that it is decidable whether or not a rewrite rule is sort
decreasing, even if the signature is not regular. \par Finally we demonstrate
that every overloaded completion procedure may also be used in the
non-overloaded world, but not conversely, and that specifications exist that
can only be completed using the non-overloaded semantics.},
}
@INPROCEEDINGS{Wand2012,
AUTHOR = {Blanchette, Jasmin Christian and Popescu, Andrei and Wand, Daniel and Weidenbach, Christoph},
EDITOR = {Beringer, Lennart and Felty, Amy},
TITLE = {More {SPASS} with {Isabelle} : Superposition with Hard Sorts and Configurable Simplification},
BOOKTITLE = {Interactive Theorem Proving : Third International Conference, ITP 2012},
PADDRESS = {Berlin},
ADDRESS = {Princeton, NJ, USA},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7406},
ISBN = {978-3-642-32346-1},
DOI = {10.1007/978-3-642-32347-8_24},
YEAR = {2012},
PAGES = {345--360},
}
@INPROCEEDINGS{WBH+02-CADE18,
AUTHOR = {Weidenbach, Christoph and Brahm, Uwe and Hillenbrand, Thomas and Keen, Enno and Theobalt, Christian and Topi{\'c}, Dalibor},
EDITOR = {Voronkov, Andrei},
TITLE = {{SPASS} Version 2.0},
BOOKTITLE = {Automated deduction, CADE-18 : 18th International Conference on Automated Deduction},
PADDRESS = {Heidelberg, Germany},
ADDRESS = {Kopenhagen, Denmark},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {2392},
ISBN = {3-540-43931-5},
YEAR = {2002},
PAGES = {275--279},
ABSTRACT = {SPASS is an automated theorem prover for full first-order logic with equality.
This system description provides an overview of recent developments in SPASS
2.0, including among others an implementation of contextual rewriting,
refinements of the clause normal form transformation, and enhancements of the
inference engine.},
}
@ARTICLE{WeberSturm:11a,
AUTHOR = {Weber, Andreas and Sturm, Thomas and Abdel-Rahman, Essam O.},
JOURNAL = {Bulletin of Mathematical Biology},
TITLE = {Algorithmic Global Criteria for Excluding Oscillations},
ADDRESS = {New York, NY},
NUMBER = {4},
PUBLISHER = {Springer},
MONTH = {April},
VOLUME = {73},
ISBN = {0092-8240},
DOI = {10.1007/s11538-010-9618-0},
YEAR = {2011},
PAGES = {899--916},
ABSTRACT = {We investigate algorithmic methods to tackle the following problem: Given a
system of parametric ordinary differential equations built by a biological
model, does there exist ranges of values for the model parameters and variables
which are both meaningful from a biological point of view and where oscillating
trajectories, can be found? We show that in the common case of polynomial
vector fields known criteria excluding the existence of non-constant limit
cycles lead to quantifier elimination problems over the reals. We apply these
criteria to various models that have been previously investigated in the
context of algebraic biology.},
}
@ARTICLE{Weidenbach1999jar,
AUTHOR = {Weidenbach, Christoph},
JOURNAL = {Journal of Automated Reasoning},
TITLE = {{SPASS V0.95TPTP}},
NUMBER = {1},
PUBLISHER = {Kluwer},
VOLUME = {23},
ISBN = {0168-7433},
YEAR = {1999},
PAGES = {21--21},
}
@PHDTHESIS{Weidenbach2000habil,
AUTHOR = {Weidenbach, Christoph},
TITLE = {{Entscheidbarkeitsprobleme f{\"u}r monadische (Horn)Klauselklassen}},
SCHOOL = {Universit{\"a}t des Saarlandes, Naturwissenschaftlich-Technische Fakult{\"a}t},
TYPE = {Habilitation thesis},
MONTH = {June},
YEAR = {2000},
ABSTRACT = {Abstract der Antrittsvorlesung:
Heute lassen sich mit modernen Beweissystemen
fuer die klassische Praedikatenlogik eine Reihe von
aktuellen Problemen wie die Analyse von Programmen oder
(Sicherheits)Protokollen vollautomatisch loesen.
Dies ist das Resultat einer Reihe von neuen Techniken/Ergebnissen,
die in Form von Kalkuelen, Redundanzkriterien, Algorithmen und
Implementierungsdesigns Einzug in aktuelle Systeme gehalten haben.
In der Vorlesung werde ich, ausgehend
von der Eingabe des Beweissystems, einer Formel, bis hin zu
seinem Resultat bei Terminierung, dem Beweis oder
der saturierten und damit erfuellbaren Klauselmenge, die
in dem SPASS-Beweissystem realisierten Techniken vorstellen und
sie aus theoretischer, pragmatischer und Implementierungssicht
diskutieren und demonstrieren.},
}
@INCOLLECTION{Weidenbach2001handbook,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Robinson, Alan and Voronkov, Andrei},
TITLE = {Combining Superposition, Sorts and Splitting},
BOOKTITLE = {Handbook of Automated Reasoning},
CHAPTER = {27},
ADDRESS = {Amsterdam, the Netherlands},
PUBLISHER = {Elsevier},
MONTH = {January},
VOLUME = {1},
YEAR = {2001},
PAGES = {1965--2013},
}
@INPROCEEDINGS{Weidenbach92a,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Ohlbach, Hans J{\"u}rgen},
TITLE = {A New Sorted Logic},
BOOKTITLE = {GWAI-92: Advances in Artificial Inteligence, Proceedings 16th German Workshop on Artificial Intelligence},
PADDRESS = {Berlin, Germany},
ADDRESS = {Bonn},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {671},
YEAR = {1993},
PAGES = {43--54},
ABSTRACT = {We present a sound and complete calculus for an expressive sorted first-order logic. Sorts are extended to the semantic and pragmatic use of unary predicates. A sort may denote an empty set and the sort structure can be created by making use of the full first-order language. Technically spoken, we allow sort declarations to be used in the same way than ordinary atoms. Therefore we can compile every first-order logic formula into our logic.\\ The extended expressivity implies an extended sorted inference machine. We present a new unification algorithm and show that the declarations the unification algorithm is built on have to be changed dynamically during the deduction process. Deductions in the resulting resolution calculus are very efficient compared to deductions in the unsorted resolution calculus. The approach is a conservative extension of the known sorted approaches, as it simplifies to the known sorted calculi if we apply the calculus to the much more restricted input formulas of these calculi.},
}
@INPROCEEDINGS{Weidenbach93a,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Bajcsy, R.},
TITLE = {Extending the Resolution Method with Sorts},
BOOKTITLE = {Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI '93)},
PADDRESS = {San Mateo, CA},
ADDRESS = {Chambery, France},
PUBLISHER = {Morgan Kaufmann},
VOLUME = {1},
YEAR = {1993},
PAGES = {60--65},
ABSTRACT = {In this paper I extend the standard first-order resolution method with special reasoning mechanisms for sorts. Sorts are one place predicates. Literals built from one place predicates are called sort literals. Negative sort literals can be compiled into restrictions of the relevant variables to sorts or can be deleted if they fulfill special conditions. Positive sort literals define the sort structure for sorted unification. Sorted unification exploits the sort restrictions of variables. As the occurrence of sort literals is not restricted, it might be necessary to add additional literals to resolvents and factors and to dynamically change the set of positive sort literals used by sorted unification during the deduction process. The calculus I propose thus extends the standard resolution method by sorted unification, residue literals and a dynamic processing of the sort information. I show that this calculus generalizes and improves existing approaches to sorted reasoning. Finally I give some applications to automated theorem proving and abduction.},
}
@INPROCEEDINGS{Weidenbach94a,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Broda, Krysia and D'Agostino, Marcello and et. al.},
TITLE = {First-Order Tableaux with Sorts},
BOOKTITLE = {TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods},
ADDRESS = {Marseille, France},
PUBLISHER = {Imperial College of Science Technology and Medicine, TR-94/5},
MONTH = {April},
YEAR = {1994},
PAGES = {247--261},
NOTE = {To appear in the Bulletin of IGPL},
ABSTRACT = {Tableau and the free variable tableau are extended with sorts. Sorts are sets of unary predicates. They can be attached to variables. Semantically, the domain of a variable is restricted to the intersection of the denotations of the attached predicates. Syntactically, the sort information is exploited by modified $\gamma$ and $\delta$ rules. The standard unification algorithm of free variable tableau is replaced by a sorted unification algorithm. The resulting calculi, tableau with sorts and free variable tableau with sorts are proved sound, complete and more suitable for mechanization than their counterparts without sorts.},
}
@INPROCEEDINGS{Weidenbach94c,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Kunze, J{\"u}rgen and Stoyan, Herbert},
TITLE = {Sorts, Resolution, Tableaux and Propositional Logic},
BOOKTITLE = {KI-94 Workshops: Extended Abstracts},
PADDRESS = {Bonn, Germany},
ADDRESS = {Saarbr{\"u}cken, Germany},
PUBLISHER = {Gesellschaft f{\"u}r Informatik},
YEAR = {1994},
PAGES = {315--316},
}
@ARTICLE{Weidenbach95d,
AUTHOR = {Weidenbach, Christoph},
JOURNAL = {Journal of the Interest Group in Pure and Applied Logics},
TITLE = {First-Order Tableaux with Sorts},
NUMBER = {6},
VOLUME = {3},
YEAR = {1995},
PAGES = {887--906},
}
@INPROCEEDINGS{Weidenbach95e,
AUTHOR = {Barth, Peter and Kleine B{\"u}ning, Hans and Weidenbach, Christoph},
EDITOR = {Dreschler-Fischer, Leonie and Pribbenow, Simone},
TITLE = {Workshop CPL Computational Propositional Logic},
BOOKTITLE = {KI-95 Activities: Workshops, Posters, Demos},
ORGANIZATION = {Gesellschaft f{\"u}r Informatik e.V.},
PADDRESS = {Bonn, Germany},
ADDRESS = {Bielefeld, Germany},
PUBLISHER = {Gesellschaft f{\"u}r Informatik},
YEAR = {1995},
PAGES = {71--72},
}
@INPROCEEDINGS{Weidenbach96a,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {McRobbie, M. A. and Slaney, J. K.},
TITLE = {Unification in Pseudo-Linear Sort Theories is Decidable},
BOOKTITLE = {Proceedings of the 13th International Conference on Automated Deduction (CADE-13)},
PADDRESS = {Berlin, Germany},
ADDRESS = {New Brunswick, USA},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1104},
ISBN = {3-540-61511-3},
YEAR = {1996},
PAGES = {343--357},
}
@INPROCEEDINGS{Weidenbach96b,
AUTHOR = {Weidenbach, Christoph and Gaede, Bernd and Rock, Georg},
EDITOR = {McRobbie, M. A. and Slaney, J. K.},
TITLE = {{SPASS} \& {FLOTTER}, Version 0.42},
BOOKTITLE = {Proceedings of the 13th International Conference on Automated Deduction (CADE-13)},
PADDRESS = {Berlin, Germany},
ADDRESS = {New Brunswick, USA},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1104},
ISBN = {3-540-61511-3},
YEAR = {1996},
PAGES = {141--145},
}
@INPROCEEDINGS{Weidenbach96c,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Schulz, Klaus U. and Kepser, Stephan},
TITLE = {Unification in Sort Theories},
BOOKTITLE = {Proceedings of the 10th International Workshop on Unification, UNIF'96},
PADDRESS = {M{\"u}nchen, Germany},
ADDRESS = {Harsching, Germany},
NUMBER = {91},
PUBLISHER = {Universit{\"a}t M{\"u}nchen},
SERIES = {CIS-Bericht},
VOLUME = {96},
YEAR = {1996},
PAGES = {16--25},
}
@INPROCEEDINGS{Weidenbach96d,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Hermann, Miki and Salzer, Gernot},
TITLE = {Sorted Unification and Its Application to Automated Theorem Proving},
BOOKTITLE = {Proceedings of the CADE-13 Workshop: Term Schematizations and Their Applications},
ADDRESS = {New Brunswick, USA},
PUBLISHER = {Self},
YEAR = {1996},
PAGES = {67--76},
NOTE = {To appear in form of a technical report at the University of Wien, Austria},
}
@PHDTHESIS{Weidenbach96e,
AUTHOR = {Weidenbach, Christoph},
TITLE = {Computational Aspects of a First-Order Logic with Sorts},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Doctoral dissertation},
YEAR = {1996},
}
@ARTICLE{Weidenbach96f,
AUTHOR = {Weidenbach, Christoph},
JOURNAL = {Annals of Mathematics and Artificial Intelligence},
TITLE = {Unification in Sort Theories and its Applications},
NUMBER = {2/4},
PUBLISHER = {Baltzer},
VOLUME = {18},
ISBN = {1012-2443},
YEAR = {1996},
PAGES = {261--293},
}
@ARTICLE{Weidenbach97jar,
AUTHOR = {Weidenbach, Christoph},
JOURNAL = {Journal of Automated Reasoning},
TITLE = {{SPASS} Version 0.49},
NUMBER = {2},
PUBLISHER = {Kluwer},
MONTH = {April},
VOLUME = {18},
ISBN = {0168-7433},
YEAR = {1997},
PAGES = {247--252},
}
@INCOLLECTION{Weidenbach98kluwer,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Bibel, Wolfgang and Schmitt, Peter H.},
TITLE = {Sorted Unification and Tree Automata},
BOOKTITLE = {Automated Deduction - A Basis for Applications},
CHAPTER = {9},
ADDRESS = {Dordrecht, The Netherlands},
PUBLISHER = {Kluwer},
MONTH = {January},
SERIES = {Applied Logic},
YEAR = {1998},
PAGES = {291--320},
}
@INCOLLECTION{Weidenbach98teubner,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Fiedler, Herbert and Gorny, Peter and Grass, Werner and H{\"o}lldobler, Steffen and Hotz, G{\"u}nter and Kerner, I. O. and Reischuk, R{\"u}diger},
TITLE = {{Rechnen in sortierter Pr{\"a}dikatenlogik}},
BOOKTITLE = {Ausgezeichnete Informatikdissertationen 1997},
ADDRESS = {Stuttgart, Germany},
PUBLISHER = {Teubner},
MONTH = {January},
YEAR = {1998},
PAGES = {183--197},
}
@INPROCEEDINGS{Weidenbach99cade,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Ganzinger, Harald},
TITLE = {Towards an Automatic Analysis of Security Protocols in First-Order Logic},
BOOKTITLE = {Proceedings of the 16th International Conference on Automated Deduction (CADE-16)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Trento, Italy},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1632},
YEAR = {1999},
PAGES = {378--382},
}
@INPROCEEDINGS{Weidenbach99cadespass,
AUTHOR = {Weidenbach, Christoph and Afshordel, Bijan and Brahm, Uwe and Cohrs, Christian and Engel, Thorsten and Keen, Enno and Theobalt, Christian and Topi{\'c}, Dalibor},
EDITOR = {Ganzinger, Harald},
TITLE = {System Description: {SPASS} Version 1.0.0},
BOOKTITLE = {Proceedings of the 16th International Conference on Automated Deduction (CADE-16)},
PADDRESS = {Berlin, Germany},
ADDRESS = {Trento, Italy},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1632},
ISBN = {3-540-66222-7},
YEAR = {1999},
PAGES = {314--318},
}
@INPROCEEDINGS{WeidenbachEtAlSpass2009,
AUTHOR = {Weidenbach, Christoph and Dimova, Dilyana and Fietzke, Arnaud and Suda, Martin and Wischnewski, Patrick},
EDITOR = {Schmidt, Renate A.},
TITLE = {{SPASS} Version 3.5},
BOOKTITLE = {Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction},
PADDRESS = {Berlin, Germany},
ADDRESS = {Montreal, Canada},
PUBLISHER = {Springer},
MONTH = {August},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {5663},
ISBN = {978-3-642-02958-5},
DOI = {10.1007/978-3-642-02959-2_10},
YEAR = {2009},
PAGES = {140--145},
}
@ARTICLE{WeidenbachMeyerEtAl98jar,
AUTHOR = {Weidenbach, Christoph and Meyer, Christoph and Cohrs, Christian and Engel, Thorsten and Keen, Enno},
JOURNAL = {Journal of Automated Reasoning},
TITLE = {{SPASS V0.77}},
NUMBER = {1},
PUBLISHER = {Kluwer},
VOLUME = {21},
ISBN = {0168-7433},
YEAR = {1998},
PAGES = {113--113},
}
@INPROCEEDINGS{WeidenbachSchmidtEtAl2007cade,
AUTHOR = {Weidenbach, Christoph and Schmidt, Renate and Hillenbrand, Thomas and Rusev, Rostislav and Topic, Dalibor},
EDITOR = {Pfenning, Frank},
TITLE = {System Description: Spass Version 3.0},
BOOKTITLE = {Automated Deduction --- CADE-21 : 21st International Conference on Automated Deduction},
PADDRESS = {Berlin, Germany},
ADDRESS = {Bremen, Germany},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {4603},
ISBN = {3-540-73594-6},
DOI = {10.1007/978-3-540-73595-3_38},
YEAR = {2007},
PAGES = {514--520},
}
@INPROCEEDINGS{WeidenbachWischnewski2012,
AUTHOR = {Weidenbach, Christoph and Wischnewski, Patrick},
TITLE = {Satisfiability Checking and Query Answering for large Ontologies},
BOOKTITLE = {PAAR-2012 : Third Workshop on Practical Aspects of Automated Reasoning},
PADDRESS = {Manchester},
ADDRESS = {Manchester, UK},
PUBLISHER = {PAAR-2012},
YEAR = {2012},
PAGES = {163--177},
}
@ARTICLE{WeidenbachWischnewskiAICom10,
AUTHOR = {Weidenbach, Christoph and Wischnewski, Patrick},
JOURNAL = {AI Communications},
TITLE = {Subterm Contextual Rewriting},
ADDRESS = {Amsterdam},
NUMBER = {2-3},
PUBLISHER = {IOS Press},
VOLUME = {23},
ISBN = {0921-7126},
DOI = {10.3233/AIC-2010-0459},
YEAR = {2010},
PAGES = {97--109},
}
@INPROCEEDINGS{WeidenbachWischnewskiCADE08,
AUTHOR = {Weidenbach, Christoph and Wischnewski, Patrick},
TITLE = {Contextual Rewriting in {SPASS}},
BOOKTITLE = {PAAR/ESHOL},
PADDRESS = {RHTW Aachen},
ADDRESS = {Sydney, Australien},
PUBLISHER = {CEUR-WS.org},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {373},
YEAR = {2008},
PAGES = {115--124},
}
@TECHREPORT{WeidenbachWischnewskiReport2009,
AUTHOR = {Weidenbach, Christoph and Wischnewski, Patrick},
TITLE = {Contextual Rewriting},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
TYPE = {Research Report},
ADDRESS = {Saarbr{\"u}cken},
NUMBER = {MPI-I-2009-RG1-002},
ISBN = {0946-011X},
YEAR = {2009},
PAGES = {29},
}
@PHDTHESIS{Wischnewski12,
AUTHOR = {Wischnewski, Patrick},
TITLE = {Efficient Reasoning Procedures for Complex First-Order Theories},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Doctoral dissertation},
ADDRESS = {Saarbr{\"u}cken},
PUBLISHER = {Universit{\"a}t des Saarlandes},
MONTH = {November},
YEAR = {2012},
}
@MASTERSTHESIS{Wischnewski2007,
AUTHOR = {Wischnewski, Patrick},
TITLE = {Contextual Rewriting in SPASS},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Master's thesis},
PUBLISHER = {Self publishing},
YEAR = {2007},
ABSTRACT = {
First-order theorem proving with equality is undecidable, in general.
However, it
is semi-decidable in the sense that it is refutationally complete. The
basis for a
(semi)-decision procedure for first-order clauses with equality is a
calculus composed
of inference and reduction rules. The inference rules of the calculus
generate
new clauses whereas the reduction rules delete clauses or transform them
into simpler
ones. If, in particular, strong reduction rules are available,
decidability of
certain subclasses of first-order logic can be shown. Hence,
sophisticated reductions
are essential for progress in automated theorem proving. In this thesis we
consider the superposition calculus and in particular the sophisticated
reduction
rule Contextual Rewriting. However, it is in general undecidable whether
contextual
rewriting can be applied. Therefore, to make the rule applicable in
practice,
it has to be further refined. In this work we develop an instance of
contextual
rewriting which effectively performs contextual rewriting and we
implement this
in the theorem prover Spass.},
}
@MASTERSTHESIS{Zimmer2007,
AUTHOR = {Zimmer, Stephan},
TITLE = {Intelligent Combination of a First Order Theorem Prover and {SMT} Procedures},
SCHOOL = {Universit{\"a}t des Saarlandes},
TYPE = {Diploma thesis},
MONTH = {December},
YEAR = {2007},
ABSTRACT = {First-order logic combined with arithmetic background theories is a
powerful tool for representing and managing huge amounts of
declarative information. Special fragments of it were successfully
applied to manifold problems from different areas of computer
science. From an automated reasoning perspective, however, this
expressiveness makes it particular challenging to develop theorem
provers that can deal with general classes of those languages:
General purpose theorem provers on the one hand cannot cope
efficiently with arithmetic and specialized decision procedures on
the other hand are notoriously bad at dealing with quantifiers, if
they are even supported at all.
The SPASS+T system, which was developed by Prevosto and Waldmann,
aims to attack this problem by combining the superposition-based
theorem prover SPASS with decision procedures for linear arithmetic
and free function symbols; furthermore, the set of standard
first-order inference and reduction rules is complemented by
specialized rules for arithmetic.
In this work we present various extensions to their initial
implementation. The main task of the thesis was to stretch the
capabilities of the system by integrating the SPASS splitting rule,
which had to be switched off so far. Splitting is highly efficient
for SPASS and has also advantages in a combination like SPASS+T. In
order to add support for splitting in SPASS+T we first revised the
previous system architecture and developed an advanced coupling
between SPASS and the SMT procedure and achieved a tighter
integration of the latter in form of a new inference rule.
Furthermore, for splitting a careful analysis of the different
prover configurations was necessary. Besides splitting, the new
coupling also allows to use the SPASS proof documentation mode
regarding subproofs that were contributed by the SMT procedure. The
documented proofs can be automatically certified. To this end we
extended the existing SPASS proof validator in such a way that it
also employs an external SMT procedure and now can verify, besides
ordinary first-order proof steps, arithmetic inferences as well. In
order to improve the built-in arithmetic simplification rules of
SPASS+T and let them also work with bignums and rational numbers, we
integrated the GNU multiple precision library. Finally, we added a
new reduction rule that deals with clauses which impose lower or
upper bounds on a variable.
We will describe all these extensions in detail, discuss their
impact on the system architecture, and demonstrate the capabilities
of the system by applying it to some examples.},
}