@STRING{addison = "Addison Wesley, Reading, MA" } @STRING{aij = "Artificial Intelligence" } @STRING{ap = "Academic Press, London" } @STRING{bi = "B.I. Wissenschaftsverlag" } @STRING{cacm = "Communications of the Association for Computing Machinery" } @STRING{cade = "Proceedings of the Conference on Automated Deduction" } @STRING{cade-10 = "Proceedings of the 10\/$^{th}$ Conference on Automated Deduction, Kaiserslautern, Germany, July 1990" } @STRING{cade-11 = "Proceedings of the 11\/$^{th}$ Conference on Automated Deduction, Saratoga Springs, NY, USA, June 1992" } @STRING{cade-12 = "Proceedings of the 12\/$^{th}$ Conference on Automated Deduction, Nancy, France, June/July 1994" } @STRING{elsevier= "Elsevier Science Publishers B.V.\ (North--Holland) Amsterdam" } @STRING{fbinformatik="Fachberichte Informatik" } @STRING{gmd = "GMD" } @STRING{gwai = "Proceedings of the German Workshop on Artificial Intelligence" } @STRING{gwai90 = "GWAI-90 --- Proceedings of the 14\/$^{th}$ German Workshop on Artificial Intelligence, Eringerfeld, September 1990" } @STRING{gwai91 = "GWAI-91 --- Proceedings of the 15\/$^{th}$ German Workshop on Artificial Intelligence, Bonn, September 1991" } @STRING{gwai92 = "GWAI-92 --- Proceedings of the 16\/$^{th}$ German Workshop on Artificial Intelligence" } @STRING{iclp = "Proceedings of the International Conference on Logic Programming" } @STRING{ijcai = "International Joint Conference on Artificial Intelligence" } @STRING{ijcai95 = "IJCAI-95 --- Proceedings of the 14\/$^{th}$ International Joint Conference on Artificial Intelligence, Montreal" } @STRING{ijcai97 = "IJCAI-97 --- Proceedings of the 15\/$^{th}$ International Joint Conference on Artificial Intelligence, Nagoya" } @STRING{inria = "Institut National de Recherche en Informatique et en Automatique" } @STRING{jar = "Journal of Automated Reasoning" } @STRING{jlp = "Journal of Logic Programming" } @STRING{jsc = "Journal of Symbolic Computation" } @STRING{jsl = "Journal of Symbolic Logic" } @STRING{lnai = "Lecture Notes in Artificial Intelligence" } @STRING{lncs = "Lecture Notes in Computer Science" } @STRING{rta = "Proceedings of the Conference on Rewriting Techniques and Applications" } @STRING{springer= "Springer Verlag, Berlin, Heidelberg, New-York" } @STRING{sri = "Stanford Research Institute (SRI)" } @STRING{sri-adr = "333 Ravenswood Ave., Menlo Parc, CA 94025" } @STRING{tcs = "Theoretical Computer Science" } @STRING{toappear= "To appear" } @STRING{tum = "Technische Universit{\"a}t M{\"u}nchen, Institut f{\"u}r Mathematik und Informatik" } @STRING{unif = "Proceedings of the International Workshop on Unification" } @STRING{unikola = "Universit{\"a}t Koblenz-Landau" } @STRING{unikolaaddress="Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz" } @InProceedings{Baumgartner:Slaney:ConstraintModellingChallenge:FTP:2009, author = {Peter Baumgartner and John Slaney}, title = {Constraint Modelling: A Challenge for Automated Reasoning}, OPTcrossref = {}, OPTkey = {}, booktitle = {FTP 2009 Workshop Proceedings}, pages = {4-18}, year = {2009}, editor = {Nicolas Peltier and Viorica Sofronie-Stokkermans}, OPTvolume = {}, number = {386}, series = {Research Report}, year = {2009}, abstract = "Cadoli et. al. noted the potential of first order automated reasoning for the purpose of analysing constraint models, and reported some encouraging initial experimental results. We are currently pursuing a very similar research program with a view to incorporating deductive technology in a state of the art constraint programming platform. Here we outline our own view of this application direction and discuss new empirical findings on a more extensive range of problems than those considered in the previous literature. While the opportunities presented by reasoning about constraint models are indeed exciting, we also find that there are formidable obstacles in the way of a practicaly useful implementation.", url = "ftp09-final.pdf", OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, publisher = {University of Oslo}, OPTnote = {}, ISBN = {82-7368-347-8}, OPTannote = {} } @Unpublished{Baumgartner:Thorstensen:IMOverview:2009, author = {Peter Baumgartner and Evgenij Thorstensen}, title = {Instance Based Methods --- An Overview}, OPTkey = {}, OPTmonth = {}, year = {2009}, abstract = "Instance-based methods are a specific class of methods for automated proof search in first-order logic. This article provides an overview of the major methods in the area and discusses their properties and relations to the more established resolution methods. It also discusses some recent trends on refinements and applications. This overview is rather brief and informal, but we provide a comprehensive literature list to follow-up on the details.", url = "IMoverview.pdf", note = {Accepted for publication in KI}, annote = unpublished } @InProceedings{Baader:etal:SAIL:TABLEAUX:2009, author = {Franz Baader and Andreas Bauer and Peter Baumgartner and Anne Cregan and Alfredo Gabaldon and Krystian Ji and Kevin Lee and David Rajaratnam and Rolf Schwitter}, title = {A Novel Architecture for Situation Awareness Systems}, OPTcrossref = {}, OPTkey = {}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009)}, pages = {77-92}, year = {2009}, editor = {Martin Giese and Aarild Waaler}, volume = {5607}, OPTnumber = {}, series = {LNAI}, OPTaddress = {}, month = {July}, OPTorganization = {}, publisher = {Springer}, abstract = "Situation Awareness (SA) is the problem of comprehending elements of an environment within a volume of time and space. It is a crucial factor in decision-making in dynamic environments. Current SA systems support the collection, filtering and presentation of data from different sources very well, and typically also some form of low-level data fusion and analysis, e.g., recognizing patterns over time. However, a still open research challenge is to build systems that support higher-level information fusion, viz., to integrate domain specific knowledge and automatically draw conclusions that would otherwise remain hidden or would have to be drawn by a human operator. To address this challenge, we have developed a novel system architecture that emphasizes the role of formal logic and automated theorem provers in its main components. Additionally, it features controlled natural language for operator I/O. It offers three logical languages to adequately model different aspects of the domain. This allows to build SA systems in a more declarative way than is possible with current approaches. From an automated reasoning perspective, the main challenges lay in combining (existing) automated reasoning techniques, from low-level data fusion of time-stamped data to semantic analysis and alert generation that is based on linear temporal logic. The system has been implemented and interfaces with Google-Earth to visualize the dynamics of situations and system output. It has been successfully tested on realistic data, but in this paper we focus on the system architecture and in particular on the interplay of the different reasoning components.", url = "SAIL-TABLEAUX-09.pdf" } @InProceedings{Baumgartner:Waldmann:MESUP:CADE:2009, author = {Peter Baumgartner and Uwe Waldmann}, title = {Superposition and Model Evolution Combined}, crossref = {CADE:09}, pages = {17-34}, address = {Montreal, Canada}, month = {July}, abstract = "We present a new calculus for first-order theorem proving with equality, MESUP, 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.", URL = "MESUP-report.pdf" } @Article{Baumgartner:etal:MEFiniteModels:JAL:2009, author = {Peter Baumgartner and Alexander Fuchs and Hans de~Nivelle and Cesare Tinelli}, title = {Computing Finite Models by Reduction to Function-Free Clause Logic}, journal = {Journal of Applied Logic}, year = {2009}, publisher = {Elsevier}, OPTkey = {}, volume = {7}, number = {1}, pages = {58-74}, month = {March}, DOI = {http://dx.doi.org/10.1016/j.jal.2007.07.005}, abstract = " Recent years have seen considerable interest in procedures for computing finite models of first-order logic specifications. One of the major paradigms, MACE-style model building, is based on reducing model search to a sequence of propositional satisfiability problems and applying (efficient) SAT solvers to them. A problem with this method is that it does not scale well because the propositional formulas to be considered may become very large. \par We propose instead to reduce model search to a sequence of satisfiability problems consisting of function-free first-order clause sets, and to apply (efficient) theorem provers capable of deciding such problems. The main appeal of this method is that first-order clause sets grow more slowly than their propositional counterparts, thus allowing for more space efficient reasoning. \par In this paper we describe our proposed reduction in detail and discuss how it is integrated into the Darwin prover, our implementation of the Model Evolution calculus. The results are general, however, as our approach can be used in principle with any system that decides the satisfiability of function-free first-order clause sets. \par To demonstrate its practical feasibility, we tested our approach on all satisfiable problems from the TPTP library. Our methods can solve a significant subset of these problems, which overlaps but is not included in the subset of problems solvable by state-of-the-art finite model builders such as Paradox and Mace4.", url = "ME-finite-models-JAL.pdf" } @InProceedings{Baumgartner:Fuchs:Tinelli:MELIA:LPAR:2008, author = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli}, title = {{ME(LIA)} -- {M}odel {E}volution {W}ith {L}inear {I}nteger {A}rithmetic {C}onstraints}, booktitle = {Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'08)}, pages = {258-273}, year = {2008}, editor = {I. Cervesato and H. Veith and A. Voronkov}, volume = {5330}, series = LNAI, url = {MELIA.pdf}, month = {November}, publisher = {Springer}, DOI = {http://dx.doi.org/10.1007/978-3-540-89439-1_19}, abstract = {Many applications of automated deduction require reasoning modulo some form of integer arithmetic. Unfortunately, theory reasoning support for the integers in current theorem provers is sometimes too weak for practical purposes. In this paper we propose a novel calculus for a large fragment of first-order logic modulo Linear Integer Arithmetic (LIA) that overcomes several limitations of existing theory reasoning approaches. The new calculus --- based on the \emph{Model Evolution} calculus, a first-order logic version of the propositional DPLL procedure --- supports restricted quantifiers, requires only a decision procedure for LIA-validity instead of a complete LIA-unification procedure, and is amenable to strong redundancy criteria. We present a basic version of the calculus and prove it sound and (refutationally) complete. } } @Article{Baumgartner:Tinelli:ModelEvolutionCalculus:AIJ:2008, author = {Peter Baumgartner and Cesare Tinelli}, title = {{T}he {M}odel {E}volution {C}alculus as a {F}irst-{O}rder {DPLL} {M}ethod}, journal = {Artificial Intelligence}, year = {2008}, url = "ME-AIJ-preprint.pdf", volume = {172}, number = {4-5}, pages = {591-632}, publisher = {Elsevier}, abstract = "The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. \par In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of {\em universal literals}, which are crucial to achieve efficiency in practice. The new calculus has been implemented successfully in the Darwin system, described elsewhere. The main results of this paper are theoretical, showing the soundness and completeness of the new calculus. In addition, the paper provides a high-level description of a proof procedure for the calculus, as well as a comparison with other calculi.", DOI = "http://dx.doi.org/10.1016/j.artint.2007.09.005" } @Proceedings{Armando:Baumgartner:Dowek:IJCAR:2008, title = {Automated Reasoning - 4th International Conference, IJCAR 2008}, year = {2008}, OPTkey = {}, booktitle = {Automated Reasoning - 4th International Conference, IJCAR 2008}, editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek}, volume = {5195}, OPTnumber = {}, series = {Lecture Notes in Artificial Intelligence}, OPTaddress = {}, month = {August}, OPTorganization = {}, publisher = {Springer}, DOI = {http://dx.doi.org/10.1007/978-3-540-71070-7}, OPTnote = {}, OPTannote = {} } @Article{Baumgartner:Furbach:Pelzer:HyperTableauxCalculusEquality:2008, author = {Peter Baumgartner and Ulrich Furbach and Bj\"orn Pelzer}, title = {The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation}, journal = {Journal of Logic and Computation}, url = {ehyper-long.pdf}, year = {2008}, abstract = {In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treat- ment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for superposition are drawn (only) from a set of positive unit clauses, and superposition inferences into positive literals is restricted into (positive) unit clauses only. The calculus also features a generic, semantically justified simplification rule which covers many redundancy elimination techniques known from superposition theorem proving. Our main results are soundness and completeness of the calculus, but we also show how to apply the calculus for finite model computation, and we briefly describe the implementation.}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, month = {November}, DOI = {http://dx.doi.org/10.1093/logcom/exn061}, OPTannote = {} } @InProceedings{Baumgartner:Furbach:Pelzer:HyperTableauxEquality:CADE:2007, author = {Peter Baumgartner and Ulrich Furbach and Bj\"orn Pelzer}, title = {Hyper Tableaux with Equality}, url = "ehyper.pdf", pages = "492-507", crossref = {CADE:07}, abstract = "In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for paramodulation are drawn (only) from a set of positive unit clauses, the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many redundancy elimination techniques known from superposition-style theorem proving. Our main theoretical result is the soundness and completeness of the calculus. The calculus is implemented, and we also report on practical experiments." } @InProceedings{Baumgartner:LogicalEngineeringInstanceBasedMethods:CADE:2007, author = {Peter Baumgartner}, title = {Logical Engineering with Instance-Based Methods}, url = "LEIM.pdf", crossref = {CADE:07}, pages = {404-409} } @InProceedings{Baumgartner:Tinelli:MEArithmetic:DagstuhlDeduction:2007, author = {Peter Baumgartner and Cesare Tinelli}, title = {Theories in Context - Model Evolution Modulo Integer Arithmetic}, booktitle = {07401 Abstracts Collection -- Deduction and Decision Procedures}, year = {2007}, editor = {Franz Baader and Byron Cook and J\"urgen Giesl and Robert Nieuwenhuis}, number = {07401}, series = {Dagstuhl Seminar Proceedings}, ISSN = {1862-4405}, publisher = {Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany}, OPTaddress = {Dagstuhl, Germany}, OPTURL = {http://drops.dagstuhl.de/opus/volltexte/2006/562}, abstract = "Some applications of automated deduction require reasoning modulo some form of integer arithmetic. Unfortunately, theory reasoning support for the integers in current theorem provers is sometimes too weak for practical purposes. In particular, the family of Satisfiability Modulo Theories solvers [NOT06] lack support for quantifiers and resort to incomplete or inefficient heuristics to deal with quantified formulas. Also, theory reasoning techniques developed within first-order theorem proving are often impractical as they require enumeration of complete sets of theory unifiers (in particular those in the tradition of Stickel's Theory Resolution [Sti85]) or feature only weak or no redundancy criteria (for instance, B{\"u}rckert's Constraint Resolution [Buer90]). In this paper we propose a novel calculus for first-order logic modulo Linear Integer Arithmetic (LIA) that avoids these problems. The calculus requires a decision procedure for the $\forall\ \exists$ fragment of LIA instead of complete LIA-unification procedure, and is amenable to strong redundancy criteria. It is derived from the Model Evolution calculus [BT03], a first-order logic version of the propositional DPLL procedure. The main data structure of that calculus is the context, which provides a compact representation of certain Herbrand interpretations. The new calculus builds in its core on a version of contexts modulo LIA. More precisely, the contexts (and the calculus) deal with conservative extensions of the integers structure by free predicate and constant symbols. In the talk we present the basic ideas of the calculus and its theoretical properties, restricted for now to the case of free predicate and constant symbols ranging over finite integer domains.", URL = "baumgartner-tinelli-dagstuhl-07.pdf", annote = "skip_html" } @InProceedings{baader_et_al:DSP:2006:562, author = {Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov}, title = {05431 Abstracts Collection -- Deduction and Applications}, booktitle = {Deduction and Applications}, year = {2006}, editor = {Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov}, number = {05431}, series = {Dagstuhl Seminar Proceedings}, ISSN = {1862-4405}, publisher = {Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany}, OPTaddress = {Dagstuhl, Germany}, URL = {http://drops.dagstuhl.de/opus/volltexte/2006/562}, note = {$<$http://drops.dagstuhl.de/opus/volltexte/2006/562$>$ [date of citation: 2006-01-01]}, OPTannote = {Keywords: Formal logic, deduction, artificial intelligence}, } @InProceedings{Baumgartner:Schmidt:BUMGEnhanced:IJCAR:2006, author = {Peter Baumgartner and Renate Schmidt}, title = {Blocking and Other Enhancements for Bottom-Up Model Generation Methods}, booktitle = {Automated Reasoning -- Third International Joint Conference on Automated Reasoning (IJCAR)}, year = {2006}, url = "BUMG-enhanced.pdf", publisher = "Springer", editor = "U. Furbach and N. Shankar", volume = "4130", pages = "125-139", series = "LNAI", abstract = "In this paper we introduce several new improvements to the bottom-up model generation (BUMG) paradigm. Our techniques are based on non-trivial transformations of first-order problems into a certain implicational form, namely range-restricted clauses. These refine existing transformations to range-restricted form by extending the domain of interpretation with new Skolem terms in a more careful and deliberate way. Our transformations also extend BUMG with a blocking technique for detecting recurrence in models. Blocking is based on a conceptually rather simple encoding together with standard equality theorem proving and redundancy elimination techniques. This provides a general-purpose method for finding small models. The presented techniques are implemented and have been successfully tested with existing theorem provers on the satisfiable problems from the TPTP library." } @InProceedings{Baumgartner:etal:MEFiniteModels:Disproving:2006, author = {Peter Baumgartner and Alexander Fuchs and and Hans de~Nivelle and Cesare Tinelli}, title = {Computing Finite Models by Reduction to Function-Free Clause Logic}, crossref = {Ahrendt:etal:Disproving:IJCAR-WS:2006}, month = {July}, abstract = " Recent years have seen considerable interest in procedures for computing finite models of first-order logic specifications. One of the major paradigms, MACE-style model building, is based on reducing model search to a sequence of propositional satisfiability problems and applying (efficient) SAT solvers to them. A problem with this method is that it does not scale well, as the propositional formulas to be considered may become very large. \par We propose instead to reduce model search to a sequence of satisfiability problems made of function-free first-order clause sets, and to apply (efficient) theorem provers capable of deciding such problems. The main appeal of this method is that first-order clause sets grow more slowly than their propositional counterparts, thus allowing for more space efficient reasoning. \par In the paper we describe the method in detail and show how it is integrated into one such prover, Darwin, our implementation of the Model Evolution calculus. The results are general, however, as our approach can used in principle with any system that decides the satisfiability of function-free first-order clause sets. \par To demonstrate its practical feasibility, we tested our approach on all satisfiable problems from the TPTP library. Our methods can solve a significant subset of these problems, which overlaps but is not included in the subset of problems solvable by state-of-the-art finite model builders such as Paradox and Mace4.", url = "ME-finite-models.pdf" } @InProceedings{Baumgartner:etal:ModelEvolutionLearning:LPAR:2006, author = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli}, title = {Lemma Learning in the Model Evolution Calculus}, url = "ME-lemma-learning.pdf", abstract = "The Model Evolution (ME) Calculus is a proper lifting to first-order logic of the DPLL procedure, a backtracking search procedure for propositional satisfiability. Like DPLL, the ME calculus is based on the idea of incrementally building a model of the input formula by alternating constraint propagation steps with non-deterministic decision steps. One of the major conceptual improvements over basic DPLL is lemma learning, a mechanism for generating new formulae that prevent later in the search combinations of decision steps guaranteed to lead to failure. We introduce three lemma generation methods for ME proof procedures, with various degrees of power, effectiveness in reducing search, and computational overhead. Even if formally correct, each of these methods presents complications that do not exist at the propositional level but need to be addressed for learning to be effective in practice for ME. We discuss some of these issues and present initial experimental results on the performance of an implementation within Darwin of the three learning procedures.", OPTcrossref = {}, OPTkey = {}, booktitle = {Logic for Programming, Artificial Intelligence and Reasoning (LPAR)}, pages = {572-586}, year = {2006}, editor = {Miki Hermann and Andrei Voronkov}, volume = {4246}, OPTnumber = {}, series = {LNAI}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, publisher = {Springer}, OPTannote = {} } @InProceedings{Baumgartner:Tinelli:ModelEvolutionCalculusEquality:CADE:2005, author = {Peter Baumgartner and Cesare Tinelli}, title = {The Model Evolution Calculus with Equality}, crossref = {CADE:05}, pages = {392-408}, url = "BaumgartnerTinelli-CADE-20.pdf", abstract = "In many theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the Model Evolution calculus (ME), a first-order version of the propositional DPLL procedure. The new calculus, MEE, is a proper extension of the ME calculus without equality. Like ME it maintains an explicit ``candidate model'', which is searched for by DPLL-style splitting. For equational reasoning MEE uses an adapted version of the ordered paramodulation inference rule, where equations used for paramodulation are drawn (only) from the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many simplification techniques known from superposition-style theorem proving. Our main result is the correctness of the MEE calculus in the presence of very general redundancy elimination criteria." } @InProceedings{Baumgartner:Suchanek:AutomatedReasoningFOOntologies:PPSWR:2006, author = {Peter Baumgartner and Fabian M. Suchanek}, title = {Automated Reasoning Support for First-Order Ontologies}, OPTkey = {}, OPTmonth = {}, year = {2006}, booktitle = {Principles and Practice of Semantic Web Reasoning 4th International Workshop (PPSWR 2006), Revised Selected Papers}, url = "PPSWR2006_long.pdf", publisher = "Springer", abstract = "Formal ontologies play an increasingly important role in demanding knowledge representation applications like the Semantic Web. Regarding automated reasoning support, the mainstream of research focusses on ontology languages that are also Description Logics, such as OWL-DL. However, many existing ontologies go beyond Description Logics and use full first-order logic. We propose a novel transformation technique that allows to apply existing model computation systems in such situations. We describe the transformation and some variants, its properties and intended applications to ontological reasoning.", editor = "J.J. Alferes and J. Bailey and W. May and U. Schwertel", volume = "4187", series = "LNAI" } @Article{Baumgartner:etal:Darwin:IJAIT:2006, author = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli}, title = {Implementing the Model Evolution Calculus}, journal = {International Journal of Artificial Intelligence Tools}, year = {2006}, editor = {Stephan Schulz and Geoff Sutcliffe and Tanel Tammet}, volume = 15, number = 1, pages = {21--52}, url = {BauFT-IJAIT-06.pdf}, } @InProceedings{ Furbach:etal:OptimizingXPathDL:INAP:2005, author = {Ulrich Furbach and Margret Gross-Hardt and Thomas Kleemann and Peter Baumgartner}, title = {{O}ptimizing the {E}valuation of {XPath} {U}sing {D}escription {L}ogics}, booktitle = {Applications of Declarative Programming and Knowledge Management (INAP/WLP 2004)}, optcrossref = {}, optkey = {}, optpages = {}, year = {2005}, editor = {Dietmar Seipel and Michael Hanus and Ulrich Geske and Oskar Bartenstein}, volume = {3392}, optnumber = {}, series = lnai, optaddress = {}, month = {March}, optorganization={}, opturl = "", publisher = springer } @Article{Baumgartner:etal:AR-KR-Management:KI:2005, author = {Peter Baumgartner and Ulrich Furbach and Adnan H. Yahya}, title = {Automated Reasoning, Knowledge Representation and Management}, journal = {KI}, year = {2005}, OPTkey = {}, volume = {1}, OPTnumber = {}, pages = {5-11}, OPTmonth = {}, OPTnote = {} } @InProceedings{Baumgartner:Mediratta:ASPPlanningBidirectional:KBCS:2004, author = {Peter Baumgartner and Anupam Mediratta}, title = {{I}mproving {S}table {M}odels {B}ased {P}lanning by {B}idirectional {S}earch}, booktitle = {International Conference on Knowledge Based Computer Systems (KBCS)}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, address = {Hyderabad, India}, month = {December}, OPTorganization = {}, OPTpublisher = {}, url = "kbcs.pdf", abstract = "Solving AI planning problems by transformation into (normal) logic programs and computing answer sets (stable models) has gained considerable interest over the last years. We investigate in this context a classical AI search technique, bidirectional search, where search is performed both from the initial facts towards the goal and vice versa. Our contribution is to show how bidirectional search can be realized in the logic programming/answer set paradigm to planning. This seems not having been investigated so far. We report on practical experiments on planning problems from an AIPS competition and show how our approach helps speeding up the planning process. We perceive our contribution mainly as a {\em technique\/} that is compatible with and complementary to existing extensions and improvements, rather than as a concrete planning system." } @InCollection{ Baumgartner:Furbach:LivingBooksStrangeThings:JS60:2004, author = {Peter Baumgartner and Ulrich Furbach}, title = {Living Books, Automated Deduction and other Strange Things}, booktitle = {Mechanizing Mathematical Reasoning: Techniques, Tools and Applications -- Essays in honour of J{\"o}rg H. Siekmann}, volume = {2605}, series = {LNCS}, pages = {255-274}, publisher = {Springer-Verlag}, year = {2004}, editor = {Dieter Hutter and Werner Stephan}, url = "http://www.dfki.de/~hutter/js60/" } @Article{ Baumgartner:EtAl:LivingBook:JAR:2004, author = "Peter Baumgartner and Ulrich Furbach and Margret Gross-Hardt and Alex Sinner", title = "{Living Book -- Deduction, Slicing, and Interaction}", journal = {Journal of Automated Reasoning}, year = {2004}, publisher = {Kluwer Academic Publishers}, volume = {32}, number = {3}, pages = {259-286}, optmonth = {}, abstract = "The Living Book is a system for the management of personalized and scenario specific teaching material. The main goal of the system is to support the active, explorative and self-determined learning in lectures, tutorials and self study. Living Book includes a course on ``Logic for Computer Scientists'' with a uniform access to various tools like theorem provers and an interactive tableau editor. It is routinely used within teaching undergraduate courses at our university. \par This paper describes both, the Living Book together with its use of theorem proving technology as a core component in the knowledge management system (KMS), and the use of this new concept in academic teaching. The KMS provides a {\em scenario management\/} component where teachers may describe those parts of given documents that are relevant in order to achieve a certain learning goal. The task of the KMS is to assemble new documents from a database of elementary units called ``slices'' (definitions, theorems, and so on) in a scenario-based way (like ``I want to prepare for an exam and need to learn about resolution''). \par The computation of such assemblies is carried out by a model-generating theorem prover for first-order logic with a default negation principle. Its input consists of meta data that describe the dependencies between different slices, and logic-programming style rules that describe the scenario-specific composition of slices. Additionally, users may assess what units they know or don't know. This information is stored in a user model, which is taken into account to compute a model that specifies the assembly of a personalized document. \par This paper introduces the e-learning context we are faced with, motivates our choice of logic, sketches the newly developed calculus used in the KMS. Finally, the application and evaluation of Living Books is presented." } @Article{ Baumgartner:Furbach:DeductionPersonalizedDocuments:AnnalsMathAI:03, author = {Peter Baumgartner and Ulrich Furbach}, title = {{Automated Deduction Techniques for the Management of Personalized Documents}}, journal = {Annals of Mathematics and Artificial Intelligence -- Special Issue on Mathematical Knowledge Management}, year = {2003}, optkey = {}, publisher = {Kluwer Academic Publishers}, volume = {38}, number = {1}, optpages = {}, optmonth = {}, url = "MKMLinzJournalFinal.pdf" , abstract = " This work is about a ``real-world'' application of automated deduction. The application is the management of documents (such as mathematical textbooks) as they occur in a readily available tool. In this ``Slicing Information Technology tool'', documents are decomposed (``sliced'') into small units. A particular application task is to assemble a new document from such units in a selective way, based on the user's current interest and knowledge. \par It is argued that this task can be naturally expressed through logic, and that automated deduction technology can be exploited for solving it. More precisely, we rely on first-order clausal logic with some default negation principle, and we propose a model computation theorem prover as a suitable deduction mechanism. \par Beyond solving the task at hand as such, with this work we contribute to the quest for arguments in favor of automated deduction techniques in the ``real world''. Also, we argue why we think that automated deduction techniques are the best choice here.", optannote = {} } @Article{ Baumgartner:Kuehn:AbducingCoreference:JLAC:00, author = "Peter Baumgartner and Michael K{\"u}hn", title = "{Abducing Coreference by Model Construction}", journal = "Journal of Language and Computation", year = {2000}, volume = {1}, number = {2}, editors = {C. Monz and M. de Rijke}, pages = {175--190}, publisher = "Hermes Science Publishers", url = "abdcoref-jlac.pdf" , abstract = "In this paper, we argue that the resolution of anaphoric expressions in an utterance is essentially an \emph{abductive} task following \cite{Hobbs:etal:InterpretationAsAbduction:AIJ:93} who use a weighted abduction scheme on horn clauses to deal with reference. We give a semantic representation for utterances containing anaphora that enables us to compute possible antecedents by abductive inference. We extend the disjunctive model construction procedure of \emph{hyper tableaux} \cite{Baumgartner:Furbach:Niemelae:HyperTableau:JELIA:96,Kuehn:RigidHyperTableaux:KI:97} with a clause transformation turning the abductive task into a model generation problem and show the completeness of this transformation with respect to the computation of abductive explanations. This abductive inference is applied to the resolution of anaphoric expressions in our general model constructing framework for incremental discourse representation which we argue to be useful for computing information updates from natural language utterances." } @Article{ Aravindan:Baumgartner:ViewDeletion:JSC:00, author = {Chandrabose Aravindan and Peter Baumgartner}, title = {Theorem Proving Techniques for View Deletion in Databases}, journal = jsc, year = {2000}, optkey = {}, volume = {29}, number = {2}, pages = {119-147}, optmonth = {}, abstract = "In this paper, we show how techniques from first-order theorem proving can be used for efficient deductive database updates. The key idea is to transform the given database, together with the update request, into a (disjunctive) logic program and to apply the hyper tableaux calculus to solve the original update problem. The resulting algorithm has the following properties: it works goal-directed (i.e.\ the search is driven by the update request), it is rational in the sense that it satisfies certain rationality postulates stemming from philosophical works on belief dynamics, and, unlike comparable approaches, it is of polynomial space complexity. \\ To obtain soundness and completeness results, the hyper tableau calculus is slightly modified for minimal model reasoning. Besides a direct proof we give an alternate proof which gives insights into the relation to previous approaches. As a by-product we thereby derive a soundness and completeness result of hyper tableaux for computing minimal abductive explanations.", url = "ftp-final.pdf" , optannote = {} } @Article{ Baumgartner:etal:TechnologicalViewPoint:KI:98, author = {Peter Baumgartner and Ingo Dahn and J{\"u}rgen Dix and Ulrich Furbach and Micha K{\"u}hn and Frieder Stolzenburg and Bernd Thomas}, title = {Automated Deduction: A Technological Point of View}, journal = {KI}, url = "ki-magazine98.pdf" , year = 1998, volume = 12, number = 4, pages = {7-14} } @Article{ Baumgartner:Furbach:Stolzenburg:RestartMEAnswers:AI:97, author = "Peter Baumgartner and Ulrich Furbach and Frieder Stolzenburg", title = "{Computing Answers with Model Elimination}", optcrossref = "", optkey = "", journal = aij, year = "1997", volume = "90", number = "1--2", pages = "135--176", url = "answers.pdf" , abstract = "We demonstrate that theorem provers using model elimination (ME) can be used as answer-complete interpreters for {\em disjunctive logic programming\/}. More specifically, we introduce a family of restart variants of model elimination, and we introduce a mechanism for computing answers. Building on this, we develop a new calculus called {\em ancestry restart ME\/}. This variant admits a more restrictive regularity restriction than restart ME, and, as a side effect, it is in particular attractive for computing definite answers. The presented calculi can also be used successfully in the context of {\em automated theorem proving}. We demonstrate experimentally that it is more difficult to compute non-trivial answers to goals than to prove the {\em existence} of answers.", optmonth = "", optannote = "" } @Article{ Baumgartner:Bruening:MESS:JAR:97, author = "Peter Baumgartner and Stefan Br{\"u}ning", title = "{A Disjunctive Positive Refinement of Model Elimination and its Application to Subsumption Deletion}", journal = jar, volume = "19", number = "2", pages = "205--262", year = {1997}, url = "RR-6-95.pdf" , abstract = "The Model Elimination (ME) calculus is a refutationally complete, goal-oriented calculus for first-order clause logic. In this paper, we introduce a new variant called {\em disjunctive positive ME (DPME)\/}; it improves on Plaisted's positive refinement of ME in that reduction steps are allowed only with positive literals stemming from clauses having at least two positive literals (so-called {\em disjunctive\/} clauses). \par DPME is motivated by its application to various kinds of {\em subsumption\/} deletion: in order to apply subsumption deletion in ME equally successful as in Resolution, it is crucial to employ a version of ME which minimizes ancestor context (i.e.\ the necessary A-literals to find a refutation). DPME meets this demand. We describe several variants of ME with subsumption, with the most important ones being {\em ME with backward and forward subsumption\/} and the {\em T$^{*}$-Context Check\/}. We compare their pruning power, also taking into consideration the well-known regularity restriction. \par All proofs are supplied. The practicability of our approach is demonstrated with experiments." } @Article{ Baumgartner:LinearizingCompletion:JAR:96, author = "Peter Baumgartner", title = "{Linear and Unit-Resulting Refutations for Horn Theories}", optcrossref = "", optkey = "", journal = jar, year = "1996", volume = "16", number = "3", pages = "241--319", month = "June", url = "lincomp.pdf" , abstract = "We present a new transformation method by which a given Horn theory is transformed in such a way that resolution derivations can be carried out which are both linear (in the sense of Prologs SLD-resolution) {\em and\/} unit-resulting (i.e.\ the resolvents are unit clauses). This is not trivial since although both strategies alone are complete, their na{{\"\i}}{}ve combination is not. Completeness is recovered by our method through a completion procedure in the spirit of Knuth-Bendix completion, however with different ordering criteria. A powerful redundancy criterion helps to find a finite system quite often. \\ The transformed theory can be used in combination with linear calculi such as e.g.\ (theory) model elimination to yield sound, complete and efficient calculi for full first order clause logic over the given Horn theory. \\ As an example application, our method discovers a generalization of the well-known linear paramodulation calculus for the combined theory of equality and strict orderings. \\ The method has been implemented and has been tested in conjunction with a model elimination theorem prover.", optnote = "", optannote = "" } @Article{ Baumgartner:etal:DeduktionUndLP:KI:96, author = "Peter Baumgartner and J{\"u}rgen Dix and Ulrich Furbach and Dorothea Sch{\"a}fer and Frieder Stolzenburg", title = "{Deduktion und Logisches Programmieren}", journal = {KI}, year = 1996, volume = 10, number = 2, pages = {34-39} } @Article{ Baumgartner:Furbach:RME:JAR:94, author = {Peter Baumgartner and Ulrich Furbach}, title = {{Model Elimination without Contrapositives and its Application to PTTP}}, journal = {Journal of Automated Reasoning}, year = {1994}, volume = {13}, pages = {339--359}, url = "nocontra-jar.pdf" , abstract = " We give modifications of model elimination which do not necessitate the use of contrapositives. These restart model elimination calculi are proven sound and complete and their implementation by PTTP is depicted. The corresponding proof procedures are evaluated by a number of runtime experiments and they are compared to other well known provers. Finally we relate our results to other calculi, namely the connection method, modified problem reduction format and Near-Horn Prolog. ", optnote = {Short version in: Proceedings of CADE-12, Springer LNAI 814, 1994, pp 87--101} } @Article{ Baumgartner:Furbach:Consolution:JSC:93, author = {Peter Baumgartner and Ulrich Furbach}, title = {{Consolution as a Framework for Comparing Calculi}}, journal = {Journal of Symbolic Computation}, year = {1993}, volume = {16}, number = {5}, publisher = {Academic Press}, url = "consolution.pdf" , pages = {445--477}, abstract = "In this paper, stepwise and nearly stepwise simulation results for a number of first-order proof calculi are presented and an overview is given that illustrates the relations between these calculi. For this purpose, we modify the {\em consolution\/} calculus in such a way that it can be instantiated to {\em resolution\/}, {\em tableaux model elimination\/}, a {\em connection method\/} and Loveland's {\em model elimination\/}. " } @InProceedings{ Baumgartner:Burchardt:LPFrameNet:JELIA:2004, author = {Peter Baumgartner and Aljoscha Burchardt}, title = {{L}ogic {P}rogramming {I}nfrastructure for {I}nferences on {F}rame{N}et}, booktitle = {Logics in Artificial Intelligence, Ninth European Conference, JELIA'04}, optcrossref = {}, optkey = {}, pages = {591--603}, year = {2004}, editor = {Jos{\'e} Alferes and Jo{\~a}o Leite}, volume = {3229}, optnumber = {}, series = lnai, optaddress = {}, optmonth = {}, optorganization={}, url = "jelia2004.pdf" , publisher = springer, abstract = "The growing size of electronically available text corpora like companies' intranets or the WWW has made \emph{information access} a hot topic within Computational Linguistics. Despite the success of statistical or keyword based methods, deeper Knowledge Representation (KR) techniques along with ``inference'' are often mentioned as mandatory, e.g.\ within the Semantic Web context, to enable e.g.\ better query answering based on ``semantical'' information. In this paper we try to contribute to the open question how to operationalize semantic information on a larger scale. As a basis we take the \emph{frame} structures of the Berkeley FrameNet~II project, which is a structured dictionary to explain the meaning of words from a lexicographic perspective. Our main contribution is a transformation of the FrameNet~II frames into the \emph{answer set programming paradigm} of logic programming. \par Because a number of different reasoning tasks are subsumed under ``inference'' in the context of natural language processing, we emphasize the flexibility of our transformation. Together with methods for automatic annotation of text documents with frame semantics which are currently developed at various sites, we arrive at an infrastructure that supports experimentation with semantic information access as is currently demanded for." } @InProceedings{ Baumgartner:etal:ModelBasedSchemaReasoning:KI:2004, author = {Peter Baumgartner and Ulrich Furbach and Margret Gross-Hardt and Thomas Kleemann}, title = {Model Based Deduction for Database Schema Reasoning}, booktitle = {KI 2004: Advances in Artificial Intelligence}, optcrossref = {}, optkey = {}, pages = {168--182}, year = {2004}, editor = {Susanne Biundo and Thom Fr{\"u}hwirth and G{\"u}nther Palm}, volume = {3238}, optnumber = {}, optseries = lncs, optaddress = {}, optmonth = {}, optorganization={}, url = "ki2004.pdf" , publisher = springer, abstract = "We aim to demonstrate that automated deduction techniques, in particular those following the model computation paradigm, are very well suited for database schema/query reasoning. Specifically, we present an approach to compute completed paths for database or XPath queries. The database schema and a query are transformed to disjunctive logic programs with default negation, using a description logic as an intermediate language. Our underlying deduction system, {\em KRHyper\/}, then detects if a query is satisfiable or not. In case of a satisfiable query, all completed paths -- those that fulfill all given constraints -- are returned as part of the computed models. \par The purpose of computing completed paths is to reduce the workload on a query processor. Without the path completion, a usual XPath query processor would search the whole database for solutions to the query, which need not be the case when using completed paths instead. \par We understand this paper as a first step, that covers a basic schema/query reasoning task by model-based deduction. Due to the underlying expressive logic formalism we expect our approach to easily adapt to more sophisticated problem settings, like type hierarchies as they evolve within the XML world." } @InProceedings{ Baumgartner:etal:Darwin:ESFOR:2004, author = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli}, title = {Darwin: A Theorem Prover for the Model Evolution Calculus}, booktitle = {Proceedings of the 1st Workshop on Empirically Successful First Order Reasoning (ESFOR'04), Cork, Ireland, 2004}, optcrossref = {}, optkey = {}, optpages = {}, year = {2004}, url = "darwin.pdf" , editor = {Stephan Schulz and Geoff Sutcliffe and Tanel Tammet}, optvolume = {}, optnumber = {}, series = {Electronic Notes in Theoretical Computer Science}, abstract = "Darwin is the first implementation of the Model Evolution Calculus by Baumgartner and Tinelli. The Model Evolution Calculus lifts the DPLL procedure to first-order logic. Darwin is meant to be a fast and clean implementation of the calculus, showing its effectiveness and providing a base for further improvements and extensions. Based on a brief summary of the Model Evolution Calculus, we describe in the main part of the paper Darwin's proof procedure and its data structures and algorithms, discussing the main design decisions and features that influence Darwin's performance. We also report on practical experiments carried out with problems from the CADE-18 and CADE-19 system competitions, as well as on results on parts of the TPTP problem library.", publisher = {Elsevier} } @InProceedings{ Baumgartner:etal:LivingBooks:WI:2003, author = {Peter Baumgartner and Ulrich Furbach and Margret Gro{\ss}-Hardt}, title = {Living Books}, booktitle = {Wirtschaftsinformatik 2003}, optcrossref = {}, optkey = {}, pages = {693--706}, year = {2003}, editor = {Wolfgang Uhr and Werner Esswein and Eric Schoop}, volume = {1}, optnumber = {}, optseries = {}, optaddress = {}, optmonth = {}, optorganization={}, publisher = {Physica-Verlag}, optannote = {} } @TechReport{Baumgartner:Fuchs:Tinelli:ModelEvolutionLearning:TechRep:2006, author = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli}, title = {Lemma Learning in the Model Evolution Calculus}, institution = {The University of Iowa}, year = {2006}, OPTkey = {}, OPTtype = {}, OPTnumber = {}, OPTaddress = {}, OPTmonth = {}, OPTnote = {}, annote = {skip_html} } @InCollection{Baumgartner:AutomatischesBeweisen:KI-Handbuch:2005, author = {Peter Baumgartner}, title = {Automatisches Beweisen}, booktitle = {Handbuch der K{\"u}nstlichen Intelligenz}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, publisher = {Oldenburg}, year = {2005}, editor = {G. G{\"o}rz, C. Rollinger and J. Schneeberger}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTtype = {}, OPTchapter = {}, OPTaddress = {}, edition = {5.}, OPTmonth = {}, note = "In Preparation", annote = {skip_html} } @Unpublished{Baumgartner:Suchanek:ModelGenerationOntologies:2005, author = {Peter Baumgartner and Fabian M. Suchanek}, title = {Model-Generation Theorem Proving for First-Order Logic Ontologies}, note = {Draft}, OPTkey = {}, OPTmonth = {}, year = {2005}, url = "model-generation-ontologies.pdf", abstract = "Formal ontologies play an increasingly important role in demanding knowledge representation applications like the {\em Semantic Web\/}. Automated reasoning support for these ontologies is mandatory for tasks like debugging, classifying or querying the knowledge bases, and description logic (DL) reasoners have been shown to be very effective for that. Yet, as language extensions beyond (decidable) DLs are being discussed, more general first-order logic systems are required, too. In this paper, we pursue this direction and consider automated reasoning on full first-order logic knowledge bases. We put forward an optimized approach of transforming such knowledge bases to clause logic. The transformations include a Brand-like transformation to eliminate equality, and a transformation that incorporates a {\em blocking\/} technique to ``checks loops'' in derivations. The latter transformation lets theorem provers terminate more often on satisfiable input formulas. It thus enables more robust automated reasoning support on ontologies, where disproving is a common task. While the transformations are applicable to any clause set, we concentrate in this paper on demonstrating their effectiveness on a standard test suite devised by the Semantic Web community.", annote = {skip_html} } @InProceedings{ Baumgartner:Tinelli:ModelEvolutionCalculus:CADE:2003, author = "Peter Baumgartner and Cesare Tinelli", title = "{The Model Evolution Calculus}", crossref = {CADE:03}, pages = {350-364}, url = "BaumgartnerTinelli-CADE-19.pdf" , abstract = "The DPLL procedure, due to Davis, Putnam, Logemann, and Loveland, is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. \par The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without recurring to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. \par In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of {\em universal literals\/}, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations." } @InProceedings{ Baumgartner:Etal:LivingBook:CADE:2003, author = {Peter Baumgartner and Ulrich Furbach and Margret Gross-Hardt and Alex Sinner}, title = {{\ttfamily\bfseries 'Living Book' :- 'Deduction', 'Slicing', 'Interaction'.} -- System Description}, crossref = "CADE:03", year = "2003", pages = "284--288", abstract = "This system description is about a real-world application of automated deduction. The system that we describe -- The Living Book -- is a tool for the management of personalized teaching material. The main goal of the Living Book system is to support the active, explorative and self-determined learning in lectures, tutorials and self study. It includes a course on 'logic for computer scientists' with a uniform access to various tools like theorem provers and an interactive tableau editor\footnote{This work is sponsored by EU IST-Grant TRIAL-SOLUTION and Bmbf-Grant In2Math.}. This course is routinely used within teaching undergraduate courses at our university." } @InProceedings{ Baumgartner:etal:LivingBook:SSGRR:2002, author = "Peter Baumgartner and Margret Gross-Hardt and Anna B. Simon", title = "{Living Book -- An Interactive and Personalized Book}", booktitle = {SSGRR 2002s - International Conference on Advances in Infrastructure for e-Business, e-Education, e-Science, and e-Medicine on the Internet}, editor = "Veljko Milutinovic", year = {2002}, publisher = "Published electronically (http://www.ssgrr.it/en/ssgrr2002s/papers.htm)", url = "living-book-an-interactive.pdf", abstract = "In the era of information technology, providing high quality and state of the art educational material is quite a challenge and requires the use of new media. The In2Math project at the University of Koblenz-Landau develops in this context the {\em Living Book\/}; Living Book means personalized user oriented educational material together with interactive components. The Living Book aims at supporting the fundamental parts of undergraduate classes in theoretical computer science. The main goal is to support the active, explorative and self-determined learning in lectures, tutorials and selfstudy. \par This paper describes the main aspects of the Living Book and explains the concepts and ideas behind it as well as the techniques used to realized these concepts. " } @InProceedings{ Baumgartner:FDPLL:CADE:00, author = "Peter Baumgartner", title = "{FDPLL -- A First-Order Davis-Putnam-Logeman-Loveland Procedure}", pages = {200--219}, crossref = {CADE:00}, url = "FDPLL-CADE-17.pdf", abstract = "FDPLL is a directly lifted version of the well-known Davis-Putnam-Logeman-Loveland (DPLL) procedure. While DPLL is based on a splitting rule for case analysis wrt.\ ground and complementary literals, FDPLL uses a lifted splitting rule, i.e.\ the case analysis is made wrt.\ non-ground and complementary literals now. \par The motivation for this lifting is to bring together successful first-order techniques like unification and subsumption to the propositionally successful DPLL procedure. \par At the heart of the method is a new technique to represent first-order interpretations, where a literal specifies truth values for all its ground instances, unless there is a more specific literal specifying opposite truth values. Based on this idea, the FDPLL calculus is developed and proven as strongly complete." } @InProceedings{ Baumgartner:Massacci:TamingXOR:CL2000:00, author = "Peter Baumgartner and Fabio Massacci", title = "{The Taming of the (X)OR}", abstract = "Many key verification problems such as bounded model-checking, circuit verification and logical cryptanalysis are formalized with combined clausal and affine logic (i.e. clauses with xor as the connective) and cannot be efficiently (if at all) solved by using CNF-only provers. \par We present a decision procedure to efficiently decide such problems. The Gauss-DPLL procedure is a tight integration in a unifying framework of a Gauss-Elimination procedure (for affine logic) and a Davis-Putnam-Logeman-Loveland procedure (for usual clause logic). \par The key idea, which distinguishes our approach from others, is the full interaction bewteen the two parts which makes it possible to maximise (deterministic) simplification rules by passing around newly created unit or binary clauses in either of these parts. We show the correcteness and the termination of Gauss-DPLL under very liberal assumptions.", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-2-2000.ps.gz" , crossref = {CL2000:00}, optkey = {}, pages = {508--522}, optyear = {}, opteditor = {}, optvolume = {}, optnumber = {}, optseries = {}, optaddress = {}, optmonth = {}, optorganization={}, optpublisher = {}, optannote = {} } @InProceedings{ Baumgartner:Kuehn:AbductiveCoreference:ICOS:99, author = {Peter Baumgartner and Michael K{\"u}hn}, title = {Abductive Coreference by Model Construction}, booktitle = {ICoS-1 Inference in Computational Semantics}, optcrossref = {}, optkey = {}, optpages = {}, year = {1999}, opteditor = {}, optvolume = {}, optnumber = {}, optseries = {}, address = {Institute for Logic, Language and Computation, University of Amsterdam}, month = {August}, optorganization={}, optpublisher = {}, optnote = {}, url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-6-99.ps.gz" , abstract = "In this paper, we argue that the resolution of anaphoric expressions in an utterance is essentially an {\em abductive\/} task following [HSAM93] who use a weighted abduction scheme on horn clauses to deal with reference. We give a semantic representation for utterances containing anaphora that enables us to compute possible antecedents by abductive inference. We extend the disjunctive model construction procedure of {\em hyper tableaux\/} [BFN96, K{\"u}h97] with a clause transformation turning the abductive task into a model generation problem and show the completeness of this transformation with respect to the computation of abuctive explanations. This abductive inference is applied to the resolution of anaphoric expressions in our general model constructing framework for incremental discourse representation [K{\"u}h99] which we argue to be useful for computing information updates from natural language utterances [Vel96]." } @InProceedings{ Baumgartner:Eisinger:Furbach:CCC:CADE:99, author = {Peter Baumgartner and Norbert Eisinger and Ulrich Furbach}, title = {A Confluent Connection Calculus}, crossref = {CADE:99}, pages = {329--343}, url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-23-98.ps.gz" , abstract = "This work is concerned with basic issues of the design of calculi and proof procedures for first-order connection methods and tableaux calculi. Proof procedures for these type of calculi developed so far suffer from not exploiting proof confluence, and very often unnecessarily rely on a heavily backtrack oriented control regime. \par As a new result, we present a variant of a connection calculus and prove its {\em strong\/} completeness. This enables the design of backtrack-free control regimes. To demonstrate that the underlying fairness condition is reasonably implementable we define an effective search strategy." } @InProceedings{ Baumgartner:Horton:Spencer:MergePathHyperTableaux:Tableaux:99, author = {Peter Baumgartner and J.D. Horton and Bruce Spencer}, title = {Merge Path Improvements for Minimal Model Hyper Tableaux}, optbooktitle = {}, crossref = {TABLEAUX:99}, optkey = {}, optpages = {}, optyear = {}, opteditor = {}, optvolume = {}, optnumber = {}, optseries = {}, optaddress = {}, optmonth = {}, optorganization={}, optpublisher = {}, optnote = {}, optannote = {}, abstract = {We combine techniques originally developed for refutational first-order theorem proving within the clause tree framework with techniques for minimal model computation developed within the hyper tableau framework. This combination generalizes well-known tableaux techniques like complement splitting and folding-up/down. We argue that this combination allows for efficiency improvements over previous, related methods. It is motivated by application to diagnosis tasks; in particular the problem of avoiding redundancies in the diagnoses of electrical circuits with reconvergent fanouts is addressed by the new technique. In the paper we develop as our main contribution in a more general way a sound and complete calculus for propositional circumscriptive reasoning in the presence of minimized and varying predicates. }, url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-1-99.ps.gz" } @InProceedings{ Baumgartner:Schaefer:CouplingKIVPROTEIN:TOOLS98:99, author = {Peter Baumgartner and Dorothea Sch{\"a}fer}, title = {Model Elimination with Simplification and its Application to Software Verification}, booktitle = {Tool Support for System Specification, Development, and Verification}, optcrossref = {}, optkey = {}, optpages = {}, publisher = {Springer-Verlag Wien NewYork}, year = {1999}, editor = {Rudolf Berghammer and Yassine Lakhnech}, series = {Advances in Computer Science}, optnumber = {}, opttype = {}, optchapter = {}, optaddress = {}, optedition = {}, optmonth = {}, optannote = {}, abstract = "This paper describes our approach of coupling the interactive software verification system KIV with the Model Elimination based, complete automated theorem prover PROTEIN. In order to make this combination work in practice, we propose to incorporate domain knowledge readily given from the KIV domain into PROTEIN. More specifically, we extend Model Elimination by a concept of simplification based on conditional rewrite rules. The extension is defined in such a way that rewrite rules as given from the KIV system can easily be accommodated. This yields better performance for proof automatization and thus relieves the system engineer from more interactions. In the paper, we describe the new simplification technique, show completeness, and demonstrate the benefits with practical experiments from the KIV domain.", url = "tools98-final-conform.pdf" } @InProceedings{ Baumgartner:HyperNextGeneration:Tableaux:98, author = "Peter Baumgartner", title = "{Hyper Tableaux --- The Next Generation}", crossref = "TABLEAUX:98", pages = "60--76", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-32-97.ps.gz" , abstract = "``Hyper tableaux'' is a sound and complete calculus for first-order clausal logic. The present paper introduces an improvement which removes the major weakness of the calculus, which is the need to (at least partially) blindly guess ground-instantiations for certain clauses. This guessing is now replaced by a unification-driven technique. \par The calculus is presented in detail, which includes a completeness proof. Completeness is proven by using a novel approach to extract a model from an open branch. This enables semantical redundancy criteria which are not present in related approaches." } @InProceedings{ Baumgartner:Furbach:RMERefinements:FTP:97, author = "Peter Baumgartner and Ulrich Furbach", title = "{Refinements for Restart Model Elimination}", url = "refinements-for-restart-model.pdf" , booktitle = "Proceedings of the International Workshop on First Order Theorem Proving (FTP 97)", series = "Technical Report", publisher = "RISC-Linz", year = "1997", month = oct, optnumber = "", optvolume = "", abstract = " We introduce and discuss a number of refinements for restart model elimination (RME). Most of these refinements are motivated by the use of RME as an interpreter for disjunctive logic programming. Especially head selection function, computation rule, strictness and independence of the goal clause are motivated by aiming at a procedural interpretation of clauses. Other refinements like regularity and early cancellation pruning are techniques to handle the tremendous search space. We discuss these techniques and investigate their compatibility. As a new result we give a proof of completeness for RME with early cancellation pruning; we furthermore show that this powerful refinement is compatibel with regularity tests. " } @InProceedings{ Aravindan:Baumgartner:ViewDeletion:ILPS:97, author = "Chandrabose Aravindan and Peter Baumgartner", title = "{A Rational and Efficient Algorithm for View Deletion in Databases}", crossref = "ILPS:97", url = "dbu.pdf", abstract = " In this paper, we show how techniques from disjunctive logic programming and classical first-order theorem proving can be used for efficient (deductive) database updates. The key idea is to tranform the given database together with the update request into a disjunctive logic program and apply disjunctive techniques (such as minimal model reasoning) to solve the original update problem. We present two variants of our algorithm both of which are of polynomial space complexity. One variant, which is based on offline preprocessing, is of polynomial time complexity. We also show that both variants are rational in the sense that they satisfy certain rationality postulates stemming from philosophical works on belief dynamics." } @InProceedings{ Baumgartner:Furbach:CalculiForDLP:ILPS:97, author = "Peter Baumgartner and Ulrich Furbach", title = "{Calculi for Disjunctive Logic Programming}", url = "ilps97-proceedings.pdf" , crossref = "ILPS:97", abstract = "We introduce a bottom-up and a top-down calculus for disjunctive logic programming (DLP). The bottom-up calculus, hyper tableaux, is depicted in its ground version and its relation to fixed point approaches from the literature is investigated. The top-down calculus, restart model elimination (RME), is presented as a sound and complete answer-computing mechanism for DLPs, and its relation to hyper tableaux is discussed. \\ In two aspect this represents an extension of SLD-resolution for Horn clause logic programming: RME {\em is\/} SLD-resolution when restricted to Horn clauses, and it has a direct counterpart to the immediate consequence operator for Horn clauses. Furthermore we discuss, that hyper tableaux can be seen as an extension of SLO-resolution." } @InProceedings{ Baumgartner:etal:TableauxDiagnosis:IJCAI:97, author = "Peter Baumgartner and Peter Fr{\"o}hlich and Ulrich Furbach and Wolfgang Nejdl", title = "{Semantically Guided Theorem Proving for Diagnosis Applications}", url = "baumgartner97semantically.pdf" , crossref = "IJCAI:97", pages = "460--465", abstract = " In this paper we demonstrate how general purpose automated theorem proving techniques can be used to solve realistic model-based diagnosis problems. For this we modify a model generating tableau calculus such that a model of a correctly behaving device can be used to guide the search for minimal diagnoses. Our experiments show that our general approach is competitive with specialized diagnosis systems." } @InProceedings{ Baumgartner:etal:TableauxDiagnosis:Tableaux:97, author = "Peter Baumgartner and Peter Fr{\"o}hlich and Ulrich Furbach and Wolfgang Nejdl", title = "{Tableaux for Diagnosis Applications}", crossref = "TABLEAUX:97", url = "baumgartner96tableaux.pdf" , pages = "76--90", abstract = "In \cite{nej96} a very efficient system for solving diagnosis tasks has been described, which is based on belief revision procedures and uses first order logic system descriptions. In this paper we demonstrate how such a system can be rigorously formalized from the viewpoint of deduction by using the calculus of hyper tableaux \cite{Baumgartner:etal:HyperTableau:JELIA:96}. The benefits of this approach are twofold: first, it gives us a clear logical description of the diagnosis task to be solved; second, as our experiments show, the approach is feasible in practice and thus serves as an example of a successful application of deduction techniques to real-world applications." } @InProceedings{ Baumgartner:Furbach:Niemelae:HyperTableau:JELIA:96, author = "Peter Baumgartner and Ulrich Furbach and Ilkka Niemel{\"a}", title = "{Hyper Tableaux}", optcrossref = "", optkey = "", opteditor = "", optvolume = "", number = "1126", series = lnai, optpages = "", booktitle = "Logics in Artificial Intelligence (JELIA '96)", year = "1996", publisher = "Springer", optaddress = "", optmonth = "", optannote = "", url = "tableaux-jelia-llncs.pdf", abstract = " This paper introduces a variant of clausal normal form tableaux that we call ``hyper tableaux''. Hyper tableaux keep many desirable features of analytic tableaux while taking advantage of the central idea from (positive) hyper resolution, namely to resolve away all negative literals of a clause in a single inference step. Another feature of the proposed calculus is the extensive use of universally quantified variables. This enables new efficient forward-chaining proof procedures for full first order theories as variants of tableaux calculi." } @InProceedings{ Baumgartner:Stolzenburg:CME:Tableaux:95, author = {Peter Baumgartner and Frieder Stolzenburg}, title = {{Constraint Model Elimination and a PTTP-Implementation}}, pages = {201--216}, url = "rheinfels.pdf" , abstract = "In constraint logic programming, proof procedures for {\em Horn} clauses are enhanced with an interface to efficient constraint solvers. In this paper we show how to incorporate constraint processing into a general, non-Horn theorem proving calculus. \par A framework for a new calculus is introduced which combines model elimination with constraint solving, following the lines of B{\"u}rckert (1991). A prototype system has been implemented rapidly by only combining a PROLOG technology implementation of model elimination and PROLOG with constraints. Some example studies, e.g. taxonomic reasoning, show the advantages and some problems with this procedure.", crossref = "TABLEAUX:95" } @InProceedings{ Baumgartner:Furbach:Stolzenburg:RestartMEAnswers:IJCAI:95, author = {Peter Baumgartner and Ulrich Furbach and Frieder Stolzenburg}, title = {{Model Elimination, Logic Programming and Computing Answers}}, crossref = "IJCAI:95", volume = {1}, pages = {335--340}, url = "ijcai-me+ans.pdf" , abstract = "We prove that theorem provers using model elimination (ME) can be used as answer complete interpreters for {\em disjunctive logic programming\/}. For this, the restart variant of ME with a mechanism for computing answers and the ancestry refinement is introduced. Furthermore, we demonstrate that in the context of {\em automated theorem proving\/} it is much more difficult to compute (non-trivial) answers to goals, instead of only proving the {\em existence\/} of answers. It holds that resolution with subsumption is {\em not\/} answer complete. We consider puzzle examples and give a comparative study of OTTER, SETHEO and our restart model elimination prover PROTEIN. " } @InProceedings{ Baumgartner:TME:ECAI:94, author = {Peter Baumgartner}, title = "{Refinements of Theory Model Elimination and a Variant without Contrapositives}", booktitle = {11th European Conference on Artificial Intelligence, ECAI 94}, year = {1994}, editor = {A.G. Cohn}, publisher = {Wiley}, url = "ecai-final.pdf" , abstract = "Theory Reasoning means to build-in certain knowledge about a problem domain into a deduction system or calculus, such as model elimination. We present several complete versions of highly restricted theory model elimination (TME) calculi. These restrictions allow (1) to keep fewer path literals in extension steps than in related calculi, and (2) to discard proof attempts with multiple occurrences of literals along a path (i.e.\ regularity holds). On the other hand, we obtain by small modifications to TME versions which do not need contrapositives ({\`a} la Near-Horn Prolog). We show how regularity can be adapted for these versions. The {\em independence of the goal computation rule\/} holds for all variants. Comparative runtime results for our PTTP-implementations are supplied.", optpages = {90--94}, optannote = { } } @InProceedings{ Baumgartner:Furbach:RME:CADE12:94, author = {Peter Baumgartner and Ulrich Furbach}, title = {{Model Elimination without Contrapositives}}, booktitle = {Automated Deduction -- CADE-12}, year = {1994}, editor = {A. Bundy}, publisher = {Springer}, pages = {87--101}, volume = {814}, series = lnai, url = "nocontra-cade-final.pdf" , abstract = " We present modifications of model elimination which do not necessitate the use of contrapositives. These restart model elimination calculi are proven sound and complete. The corresponding proof procedures are evaluated by a number of runtime experiments and they are compared to other well known provers. Finally we relate our results to other calculi, namely the connection method, modified problem reduction format and Near-Horn Prolog. " } @InProceedings{ Baumgartner:Furbach:PROTEIN:CADE12:94, author = {Peter Baumgartner and Ulrich Furbach}, title = {{PROTEIN: A {\em PRO\/}ver with a {\em T\/}heory {\em E\/}xtension {\em I\/}nterface}}, booktitle = {Automated Deduction -- CADE-12}, year = {1994}, editor = {A. Bundy}, publisher = {Springer}, pages = {769--773}, volume = {814}, series = lnai, url = "protein-cade-final.pdf" , abstract = "PROTEIN ({\em PRO\/}ver with a {\em T\/}heory {\em E\/}xtension {\em IN\/}terface) is a PTTP-based first order theorem prover over built-in theories. Besides various standard-refinements known for model elimination, PROTEIN also offers a variant of model elimination for case-based reasoning and which does not need contrapositives. ", optnote = "Available in the WWW, URL: {\small\tt http://www.uni-koblenz.de/ag-ki/Systems/PROTEIN/}" } @InProceedings{ Baumgartner:OrderedTheoryResolution:LPAR:92, author = {Peter Baumgartner}, title = "{An Ordered Theory Resolution Calculus}", booktitle = {Logic Programming and Automated Reasoning (Proceedings)}, year = {1992}, month = {July}, editor = {A. Voronkov}, publisher = {Springer}, address = {St. Petersburg, Russia}, pages = {119--130}, series = lnai, volume = "624", url = "lparfinal.pdf" , abstract = "In this paper we present an ordered theory resolution calculus and prove its completeness. Theory reasoning means to relieve a calculus from explicitly drawing inferences in a given theory by special purpose inference rules (e.g. E-resolution for equality reasoning). We take advantage of orderings (e.g. simplification orderings) by disallowing to resolve upon clauses which violate certain maximality constraints; stated positively, a resolvent may only be built if all the selected literals are maximal in their clauses. By this technique the search space is drastically pruned. As an instantiation for theory reasoning we show that equality can be built in by rigid E-unification. " } @InProceedings{ Baumgartner:TME:GWAI:92, author = {Peter Baumgartner}, title = "{A Model Elimination Calculus with Built-in Theories}", booktitle = gwai92, url = "gwai-final.pdf" , year = {1992}, editor = {H.-J. Ohlbach}, publisher = {Springer}, pages = {30--42}, series = lnai, volume = "671", abstract = "The {\em model elimination calculus} is a linear, refutationally complete calculus for first order clause logic. We show how to extend this calculus with a framework for {\em theory reasoning}. Theory reasoning means to separate the knowledge of a given domain or theory and treat it by special purpose inference rules. We present two versions of theory model elimination: the one is called {\em total theory model elimination} (which allows e.g. to treat equality in a rigid E-resolution style), and the other is called {\em partial theory model elimination} (which allows e.g. to treat equality in a paramodulation style). " } @InProceedings{ Baumgartner:91a, author = {Peter Baumgartner}, title = {{A Completeness Proof Technique for Resolution with Equality}}, booktitle = {GWAI '91 -- 15. Fachtagung f{\"u}r K{\"u}nstliche Intelligenz}, year = 1991, editor = {Th. Christaller}, publisher = {Springer}, pages = {12--22}, note = {Informatik Fachberichte 285}, annote = {11 Seiten} } @InProceedings{ Baumgartner:90b, author = {Peter Baumgartner}, title = {{Combining Horn Clause Logic with Rewrite Rules}}, booktitle = {{Artificial Intelligence IV -- Methodology, Systems, Applications}}, year = {1990}, editor = {Ph. Jorrand, V. Sgurev}, publisher = {Norh Holland}, annote = {We show how to extend a Horn clause specification with equality, where the equational theory is defined by a canonical term rewrite system. This is achieved by a transformation scheme which directly builds in a theory unification procedure a la narrowing into the Horn clauses. The advantages of this approach are, for the first, its independency from the calculus, and for the second, the directed and thus very efficient treatment of equality.} } @Book{ Baumgartner:TheoryReasoningConnectionCalculi:LNAI:98, author = "Peter Baumgartner", title = "{Theory Reasoning in Connection Calculi}", publisher = "Springer", year = "1998", optcrossref = "", optkey = "", volume = "1527", optnumber = "", series = lnai, url = "diss-baumgartner.ps", optaddress = "", optedition = "", optmonth = "", optannote = "" } @InProceedings{ Baumgartner:Petermann:TheoryReasoning:DFGBook:98, author = "Peter Baumgartner and Uwe Petermann", title = "{Chapter II.6: Theory Reasoning}", chapter = "Special Calculi and Refinements", crossref = "Bibel:Schmitt:DFGBook:98", optkey = "", optpublisher = "", optyear = "", opteditor = "", pages = "191--224", volume = "I: Foundations. Calculi and Refinements", optnumber = "", optseries = "", optaddress = "", optedition = "", optmonth = "", opttype = "", optnote = "", optannote = "" } @InCollection{ Baumgartner:FDPLL:IJCAIBook:02, author = {Peter Baumgartner}, title = {{A First-Order Logic Davis-Putnam-Logemann-Loveland Procedure}}, booktitle = {AI in the new Millenium}, optpages = {}, publisher = {Morgan Kaufmann}, year = {2002}, editor = {Gerhard Lakemeyer and Bernhard Nebel}, url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-3-2002.pdf" , optchapter = {}, optaddress = {}, optmonth = {}, note = {{\bfseries This book contains the contributions to the International Joint Conference on Artificial Intelligence (IJCAI 2001) distinguished paper track.}}, optannote = {} } @InProceedings{ Baumgartner:Furbach:VariantsClausalTableaux:DFGBook:98, author = "Peter Baumgartner and Ulrich Furbach", title = "{Chapter I.3: Variants of Clausal Tableaux}", crossref = "Bibel:Schmitt:DFGBook:98", optkey = "", optpublisher = "", optyear = "", opteditor = "", pages = "73--102", volume = "I: Foundations. Calculi and Refinements", optnumber = "", optseries = "", optaddress = "", optedition = "", optmonth = "", opttype = "", optnote = "", optannote = "" } @InCollection{ Baumgartner:Eisinger:Furbach:CCC:WB60:99, author = {Peter Baumgartner and Norbert Eisinger and Ulrich Furbach}, title = {A Confluent Connection Calculus}, booktitle = {Intellectics and Computational Logic -- Papers in Honor of Wolfgang Bibel}, optpages = {}, publisher = {Kluwer}, year = {1999}, editor = {Steffen H{\"o}lldobler}, url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-23-98.ps.gz" , optchapter = {}, optaddress = {}, optmonth = {}, optnote = {}, optannote = {}, abstract = "This work is concerned with basic issues of the design of calculi and proof procedures for first-order connection methods and tableaux calculi. Proof procedures for these type of calculi developed so far suffer from not exploiting proof confluence, and very often unnecessarily rely on a heavily backtrack oriented control regime. \par As a new result, we present a variant of a connection calculus and prove its {\em strong\/} completeness. This enables the design of backtrack-free control regimes. To demonstrate that the underlying fairness condition is reasonably implementable we define an effective search strategy. We show that with the new approach the search space can be exponentially smaller than those of current, backtracking-oriented proof procedures based on {\em weak\/} completeness results." } @TechReport{ baumgartner:etal:5:2004, author = "Peter Baumgartner and Ulrich Furbach and Margret Gro{\ss}-Hardt and Thomas Kleemann", title = "{Model Based Deduction for Database Schema Reasoning}", institution = "{Universit{\"a}t Koblenz-Landau}", year = 2004, type = "Fachberichte Informatik", number = "5--2004", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Universit{\"a}tsstr. 1, D-56070 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-5-2004.pdf" , abstract = "We aim to demonstrate that automated deduction techniques, in particular those following the model computation paradigm, are very well suited for database schema/query reasoning. Specifically, we present an approach to compute completed paths for database or XPath queries. The database schema and a query are transformed to disjunctive logic programs with default negation, using a description logic as an intermediate language. Our underlying deduction system, KRHyper, then detects if a query is satisfiable or not. In case of a satisfiable query, all completed paths -- those that fulfill all given constraints -- are returned as part of the computed models.\par The purpose of our approach is to dramatically reduce the workload on the query processor. Without the path completion, a usual XML query processor would search the database for solutions to the query.\par In the paper we describe the transformation in detail and explain how to extract the solution to the original task from the computed models.\par We understand this paper as a first step, that covers a basic schema/query reasoning task by model-based deduction. Due to the underlying expressive logic formalism we expect our approach to easily adapt to more sophisticated problem settings, like type hierarchies as they evolve within the XML world.", annote = "skip_html" } @Article{ Baumgartner:etal:in2math:swtechnik:2004, author = {Peter Baumgartner and Barbara Grabowski and Walter Oevel and Erica Melis}, title = {{I}n2Math - {I}nteraktive {M}athematik- und {I}nformatikgrundausbildung}, journal = {Softwaretechnik-Trends}, year = {2004}, optkey = {}, url = "http://www.uni-koblenz.de/~peter/Publications/in2math.pdf", volume = {24}, number = {1}, pages = {36-45}, optmonth = {}, optnote = {}, optannote = {} } @InProceedings{ Baumgartner:etal:KRHyperInsideModelBasedDeductionApplications:CADE-19-WS:2003, author = {Peter Baumgartner and Ulrich Furbach and Margret Gross-Hardt and Thomas Kleemann and Christoph Wernhard}, title = {KRHyper Inside --- Model Based Deduction in Applications}, booktitle = {Proc.\ CADE-19 Workshop on Novel Applications of Deduction Systems}, optcrossref = {}, optkey = {}, optpages = {}, year = {2003}, url = "novel.pdf", opteditor = {}, optvolume = {}, optnumber = {}, optseries = {}, optaddress = {}, optmonth = {}, optorganization={}, optpublisher = {}, optnote = {}, optannote = {}, abstract = "Three real world applications are depicted which all have in common, that their core component is a full first order theorem prover, based on the hyper tableau calculus. These applications concern information retrieval in electronic publishing, the integration of description logics with other knowledge representation techniques and XML query processing." } @TechReport{ baumgartner:etal:13:2003, author = "Peter Baumgartner and Ulrich Furbach and Margret Gross-Hardt and Alex Sinner", title = "{'Living Book' :- 'Deduction', 'Slicing', 'Interaction'.}", institution = "{Universit{\"a}t Koblenz-Landau}", year = "{2003}", type = "Fachberichte Informatik", number = "13--2003", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-13-2003.pdf" , abstract = "This system description is about a real-world application of automated deduction. The system that we describe -- The Living Book -- is a tool for the management of personalized teaching material. The main goal of the Living Book system is to support the active, explorative and self-determined learning in lectures, tutorials and self study. It includes a course on 'logic for computer scientists' with a uniform access to various tools like theorem provers and an interactive tableau editor. This course is routinely used within teaching undergraduate courses at our university. ", annote = "skip_html" } @TechReport{ baumgartner:etal:6:2003, author = "Peter Baumgartner and Ulrich Furbach and Margret Gro{\ss}-Hardt", title = "{Living Books}", institution = "{Universit{\"a}t Koblenz-Landau}", year = "{2003}", type = "Fachberichte Informatik", number = "6--2003", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-6-2003.pdf" , abstract = "In this paper we introduce a personalized way of presenting learning material, which is in particular suited for the use in e-Learning environments. We will explain the knowledge-based aspects of this technology, and we demonstrate with an example the additional feature of interactivity, by which the approach deserves the name 'Living Book'. The various possibilities of using Living Books in university teaching are discussed.", annote = "skip_html" } @TechReport{ baumgartner:etal:2:2003, author = "Peter Baumgartner and Margret Gross-Hardt and Alex Sinner", title = "{Living Book -- Deduction, Slicing, and Interaction}", institution = "{Universit{\"a}t Koblenz-Landau}", year = "{2003}", type = "Fachberichte Informatik", number = "2--2003", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-2-2003.pdf" , abstract = "The Living Book is a system for the management of personalized and scenario specific teaching material. The main goal of the system is to support the active, explorative and self-determined learning in lectures, tutorials and self study. The Living Book includes a course on 'logic for computer scientists' with a uniform access to various tools like theorem provers and an interactive tableau editor. It is routinely used within teaching undergraduate courses at our university. \par This paper describes the Living Book and the use of theorem proving technology as a core component in the knowledge management system (KMS) of the Living Book. The KMS provides a {\em scenario management\/} component where teachers may describe those parts of given documents that are relevant in order to achieve a certain learning goal. The task of the KMS is to assemble new documents from a database of elementary units called 'slices' (definitions, theorems, and so on) in a scenario-based way (like 'I want to prepare for an exam and need to learn about resolution'). \par The computation of such assemblies is carried out by a model-generating theorem prover for first-order logic with a default negation principle. Its input consists of meta data that describe the dependencies between different slices, and logic-programming style rules that describe the scenario-specific composition of slices. Additionally, a user model is taken into account that contains information about topics and slices that are known or unknown to a student. A model computed by the system for such input then directly specifies the document to be assembled. \par This paper introduces the e-learning context we are faced with, motivates our choice of logic and presents the newly developed calculus used in the KMS.", annote = "skip_html" } @TechReport{ baumgartner:tinelli:1:2003, author = "Peter Baumgartner and Cesare Tinelli", title = "{The Model Evolution Calculus}", institution = "{Universit{\"a}t Koblenz-Landau}", year = "{2003}", type = "Fachberichte Informatik", number = "1--2003", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-1-2003.pdf" , abstract = "The DPLL procedure, due to Davis, Putnam, Logemann, and Loveland, is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. \par The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without recurring to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. \par In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of {\em universal literals\/}, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations." } @TechReport{ baumgartner:3:2002, author = "Peter Baumgartner", title = "{A First-Order Logic Davis-Putnam-Logemann-Loveland Procedure}", institution = "{Universit{\"a}t Koblenz-Landau}", year = "{2002}", type = "Fachberichte Informatik", number = "3--2002", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-3-2002.pdf" , abstract = " The Davis-Putnam-Logemann-Loveland procedure (DPLL) was introduced in the early 60s as a proof procedure for first-order logic. Nowadays, only its propositional logic core component is widely used in efficient propositional logic provers and respective applications. This success motivates to reconsider lifting DPLL to the first-order logic level in a more contemporary way, by exploiting successful first-order techniques like ``unification''. Following this idea, in this paper a first-order logic version of DPLL, FDPLL, is presented. \par While propositional DPLL is based on a splitting rule for case analysis wrt.\ ground and complementary literals, FDPLL uses a lifted splitting rule, i.e.\ the case analysis is made wrt.\ non-ground and complementary literals now. To make this work, a new way of treating variables is employed. It comes together with a compact way of representing and reasoning with first-order logic interpretations, much like propositional DPLL reasons about propositional truth assignments. As a nice consequence, FDPLL naturally decides the class of Bernays-Sch{\"o}nfinkel formulas, which is notoriously difficult for most other calculi." } @InProceedings{ Baumgartner:Furbach:Thomas:ModelBasedDeductionForKR:WLP:2002, author = {Peter Baumgartner and Ulrich Furbach and Bernd Thomas}, title = {Model Based Deduction for Knowledge Representation}, booktitle = {17. WLP: Workshop Logische Programmierung, {TU} {D}resden, {D}ecember 11--13, 2002}, pages = {156-166}, year = {2002}, editor = {Bertram Fronh\"ofer and Steffen H\"olldobler}, number = {TUD--FI03--03}, series = {Technische Berichte der Fakult\"at Informatik}, month = {April}, organization = {TU Dresden, 01062 Dresden}, note = {ISSN 1430--211X}, url = "LP-workshop.pdf" } @InProceedings{ Baumgartner:Furbach:ModelBasedDeductionForKR:SemanticWeb:2002, author = {Peter Baumgartner and Ulrich Furbach}, title = {Model Based Deduction for Knowledge Representation (Position Paper)}, booktitle = {International Workshop on the Semantic Web, Workshop at WWW2002}, optcrossref = {}, optkey = {}, optpages = {}, year = {2002}, editor = {Martin Frank, Natasha Noy,Steffen Staab}, optvolume = {}, optnumber = {}, optseries = {}, optaddress = {}, optmonth = {}, optorganization={}, optpublisher = {}, optnote = {}, annote = {Online-Proceedings available at \texttt{http://semanticweb2002.aifb.uni-karlsruhe.de/programme.htm}} } @Misc{ Baumgartner:KMSDeliverable:2001, optkey = {}, author = {Peter Baumgartner}, title = {{Knowledge Management System}}, opthowpublished={}, optmonth = {}, optyear = {}, note = {Trial-Solution project deliverable}, url = {KMS-deliverable.pdf} , optannote = {} } @TechReport{ baumgartner:furbach:2:2002, author = "Peter Baumgartner and Ulrich Furbach", title = "{Automated Deduction Techniques for the Management of Personalized Documents}", institution = "{Universit{\"a}t Koblenz-Landau}", year = "{2002}", type = "Fachberichte Informatik", number = "2--2002", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-2-2002.pdf" , abstract = " This work is about a ``real-world'' application of automated deduction. The application is the management of documents (such as mathematical textbooks) as they occur in a readily available tool. In this ``Slicing Information Technology tool'', documents are decomposed (``sliced'') into small units. A particular application task is to assemble a new document from such units in a selective way, based on the user's current interest and knowledge. \par It is argued that this task can be naturally expressed through logic, and that automated deduction technology can be exploited for solving it. More precisely, we rely on first-order clausal logic with some default negation principle, and we propose a model computation theorem prover as a suitable deduction mechanism. \par Beyond solving the task at hand as such, with this work we contribute to the quest for arguments in favor of automated deduction techniques in the ``real world''. Also, we argue why we think that automated deduction techniques are the best choice here.", annote = "skip_html" } @InProceedings{ Baumgartner:Blohm:MKM:01, author = {Peter Baumgartner and Antje Blohm}, title = {Automated Deduction Techniques for the Management of Personalized Documents}, booktitle = {Proc. of {\em MKM 2001 -- First International Workshop on Mathematical Knowledge Management\/}}, url = "MKMLinzFinal.pdf", year = {2001}, address = {Linz, Austria}, optkey = {} } @Unpublished{ Baumgartner:Blohm:GrossHardt:OMDocIssues:OpenMathWs:01, author = {Peter Baumgartner and Antje Blohm and Margret Gross-Hardt}, title = {OMDoc in Use -- Experiences and issues in mathematical knowledge management}, note = {{\em OpenMath Workshop\/}, Linz, Austria, September 2001}, optkey = {}, optmonth = {}, optyear = {}, optannote = {} } @InProceedings{ Baumgartner:DeductionPersonalizedDokuments:FutureDirections:01, author = {Peter Baumgartner}, title = {Automated Deduction Techniques for the Management of Personalized Documents}, booktitle = {Proc. of the IJCAR-Workshop {\em Future Directions in Automated Reasoning}}, url = "CadeWSFutureDirectionsFinal.ps.gz", year = {2001}, address = {Siena, Italy}, optkey = {}, editor = {Manfred Kerber} } @TechReport{ baumgartner:zhang:5:2000, author = "Peter Baumgartner and Hantao Zhang~(Eds.)", title = "{FTP 2000 -- Third International Workshop on First-Order Theorem Proving, St Andrews, Scotland, July 2000}", institution = "Universit{\"a}t Koblenz-Landau", year = "2000", type = "Fachberichte Informatik", number = "5--2000", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-5-2000/" , abstract = "FTP 2000 is the third in a series of workshops on First-Order Theorem Proving. Following the successes of the first workshop (FTP'97) in RISC Linz, Schloss Hagenberg, Austria, and the second (FTP'98) in Vienna, Austria, this year's workshop will be held in St Andrews, Scotland, in conjunction with {\em Tableaux 2000\/}, the major international conference for automated reasoning with analytic tableaux and related methods ({\tt http://i12www.ira.uka.de/TABLEAUX/}). Like the preceding workshops in this series, FTP 2000 provides a forum for presentation of recent work and discussion of research in progress on First-order Theorem Proving as a core theme of automated deduction. More information about the FTP workshop series is available from the web page {\tt http://www.logic.at/FTP/}. \par The technical program of FTP 2000 consists of three invited talks, 18 regular papers, and two position papers. The topics of these papers match very well those of the workshop which cover automated theorem proving in first-order classical, many-valued, and modal logics, including nonexclusively: resolution, equational reasoning, term-rewriting, model construction, constraint reasoning, unification, propositional logic, specialized decision procedures; strategies and complexity of theorem proving procedures; and applications of first-order theorem provers to problems in verification, artificial intelligence, and mathematics." } @TechReport{ baumgartner:massacci:2:2000, author = "Peter Baumgartner and Fabio Massacci", title = "{The Taming of the (X)OR}", institution = "Universit{\"a}t Koblenz-Landau", year = "2000", type = "Fachberichte Informatik", number = "2--2000", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-2-2000.pdf" , abstract = "Many key verification problems such as bounded model-checking, circuit verification and logical cryptanalysis are formalized with combined clausal and affine logic (i.e.\ clauses with xor as the connective) and cannot be efficiently (if at all) solved by using CNF-only provers. \par We present a decision procedure to \emph{efficiently} decide such problems. The Gauss-DPLL procedure is a tight integration in a unifying framework of a Gauss-Elimina\-tion procedure (for affine logic) and a Davis-Putnam-Logeman-Loveland procedure (for usual clause logic). \par The key idea, which distinguishes our approach from others, is the full interaction bewteen the two parts which makes it possible to maximise (deterministic) simplification rules by passing around newly created unit or binary clauses in either of these parts. We show the correcteness and the termination of Gauss-DPLL under very liberal assumptions.", annote = "skip_html" } @TechReport{ baumgartner:kuehn:6:99, author = "Peter Baumgartner and Michael K{\"u}hn", title = "{Abductive Coreference by Model Construction}", institution = "Universit{\"a}t Koblenz-Landau", year = "1999", type = "Fachberichte Informatik", number = "6--99", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-6-99.ps.gz" , abstract = "In this paper, we argue that the resolution of anaphoric expressions in an utterance is essentially an {\em abductive\/} task following [HSAM93] who use a weighted abduction scheme on horn clauses to deal with reference. We give a semantic representation for utterances containing anaphora that enables us to compute possible antecedents by abductive inference. We extend the disjunctive model construction procedure of {\em hyper tableaux\/} [BFN96, K{\"u}h97] with a clause transformation turning the abductive task into a model generation problem and show the completeness of this transformation with respect to the computation of abuctive explanations. This abductive inference is applied to the resolution of anaphoric expressions in our general model constructing framework for incremental discourse representation [K{\"u}h99] which we argue to be useful for computing information updates from natural language utterances [Vel96].", annote = "skip_html" } @TechReport{ baumgartner:etal:1:99, author = "Peter Baumgartner and J.D. Horton and Bruce Spencer", title = "{Merge Path Improvements for Minimal Model Hyper Tableaux}", institution = "Universit{\"a}t Koblenz-Landau", year = "1999", type = "Fachberichte Informatik", number = "1--99", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-1-99.ps.gz" , abstract = "We combine techniques originally developed for refutational first-order theorem proving within the clause tree framework with techniques for minimal model computation developed within the hyper tableau framework. This combination generalizes well-known tableaux techniques like complement splitting and folding-up/down. We argue that this combination allows for efficiency improvements over previous, related methods. It is motivated by application to diagnosis tasks; in particular the problem of avoiding redundancies in the diagnoses of electrical circuits with reconvergent fanouts is addressed by the new technique. In the paper we develop as our main contribution in a more general way a sound and complete calculus for propositional circumscriptive reasoning in the presence of minized and varying predicates.", annote = "skip_html" } @TechReport{ baumgartner:etal:23:98, author = "Peter Baumgartner and Norbert Eisinger and Ulrich Furbach", title = "{A Confluent Connection Calculus}", institution = "Universit{\"a}t Koblenz-Landau", year = "1998", type = "Fachberichte Informatik", number = "23--98", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-23-98.ps.gz" , abstract = "This work is concerned with basic issues of the design of calculi and proof procedures for first-order connection methods and tableaux calculi. Proof procedures for these type of calculi developed so far suffer from not exploiting proof confluence, and very often unnecessarily rely on a heavily backtrack oriented control regime. \par As a new result, we present a variant of a connection calculus and prove its {\em strong\/} completeness. This enables the design of backtrack-free control regimes. To demonstrate that the underlying fairness condition is reasonably implementable we define an effective search strategy. We show that with the new approach the search space can be exponentially smaller than those of current, backtracking-oriented proof procedures based on {\em weak\/} completeness results.", annote = "skip_html" } @InProceedings{ Baumgartner:Schaefer:ProblemSolvingWS:CADE:98, author = {Peter Baumgartner and Dorothea Sch{\"a}fer}, title = {Model Elimination with Simplification and its Application to Software Verification}, booktitle = {CADE-15 Workshop on Problem-solving Methodologies with Automated Deduction}, year = {1998}, note = "http://www.uni-koblenz.de/{\textasciitilde}peter/cade-15-ws/" , optkey = {}, editor = {Peter Baumgartner and Ulrich Furbach and Michael Kohlhase and William McCune and Wolfgang Reif and Mark Stickel and Tom{\`a}s Uribe} } @TechReport{ Baumgartner:Schaefer:5:98, author = "Peter Baumgartner and Dorothea Sch{\"a}fer", title = "{Model Elimination with Simplification and its Application to Software Verification}", institution = "Universit{\"a}t Koblenz-Landau", year = "1998", type = "Fachberichte Informatik", number = "5--98", language = "english", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-5-98.ps.gz" , abstract = " This work is motivated by a coupling of the interactive software verification system KIV \cite{Reif:Schellhorn:Stenzel:KIV:CADE:97} with our Model Elimination prover PROTEIN \cite{Baumgartner:Furbach:PROTEIN:CADE12:94}. In order to make this combination efficient, we extend Model Elimination by a concept of simplification based on conditional rewrite rules. The extension is defined in such a way that rewrite rules as given from the KIV system can easily be accommodated. In the paper, we describe the new simplification technique, discuss completeness, and demonstrate with practical practical experiments from the KIV domain the benefits.", annote = "skip_html" } @TechReport{ baumgartner:32:97, author = "Peter Baumgartner", title = "{Hyper Tableaux --- The Next Generation}", institution = "Universit{\"a}t Koblenz-Landau", year = "1997", type = "Fachberichte Informatik", number = "32--97", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-32-97.ps.gz" , abstract = "``Hyper tableaux'' is a sound and complete calculus for first-order clausal logic. The present paper introduces an improvement which removes the major weakness of the calculus, which is the need to (at least partially) blindly guess ground-instantiations for certain clauses. This guessing is now replaced by a unification-driven technique. \par The calculus is presented in detail, which includes a completeness proof. Completeness is proven by using a novel approach to extract a model from an open branch. This enables semantical redundancy criteria which are not present in related approaches.", annote = "skip_html" } @TechReport{ baumgartner:23:97, author = "Peter {Baumgartner~(Hrsg.)}", title = "{Jahrestreffen der GI-Fachgruppe 1.2.1 `Deduktionssysteme' --- Kurzfassungen der Vortr{\"a}ge}", institution = "Universit{\"a}t Koblenz-Landau", year = "1997", type = "Fachberichte Informatik", number = "23--97", language = "german", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-23-97.ps.gz" , abstract = "Das Jahrestreffen 1997 der GI-Fachgruppe 1.2.1 `Deduktionssysteme' --- besser bekannt als `Deduktionstreffen' --- fand vom 30.9.\ bis 2.10.\ 1997 in Schloss Dagstuhl statt. Die Organisation wurde dieses Jahr von der KI-Gruppe an der Universit{\"a}t Koblenz-Landau (Leitung Prof.~Furbach) {{\"u}}bernommen." } @TechReport{ aravindan:baumgartner:10:97, author = "Chandrabose Aravindan and Peter Baumgartner", title = "{A Rational and Efficient Algorithm for View Deletion in Databases}", institution = "Universit{\"a}t Koblenz-Landau", year = "1997", type = "Fachberichte Informatik", number = "10--97", language = "english", address = "Universit{\"a}t Koblenz-Landau, Institut f{\"u}r Informatik, Rheinau 1, D-56075 Koblenz", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-10-97.ps.gz" , abstract = "", annote = "skip_html" } @Misc{ Baumgartner:Habil:2002, optkey = {}, author = {Peter Baumgartner}, title = {{Automatische Deduktion -- Von Kalk{\"u}len zu Anwendungen}}, howpublished = {Habilitation thesis, University of Koblenz-Landau, Germany}, optmonth = {}, year = {2002}, note = {(in German)}, optannote = {} } @PhDThesis{ Baumgartner:TheoryReasoning:PhDThesis:96, author = "Peter Baumgartner", title = "{Theory Reasoning in Connection Calculi and the Linearizing Completion Approach}", school = unikola, year = "1996", url = "diss-baumgartner.pdf", optcrossref = "", optkey = "", optaddress = "", optmonth = "", opttype = "", abstract = "This thesis is on extensions of calculi for automated theorem proving towards theory reasoning. It focuses on connection methods\index{Connection!Method} and in particular on theory model elimination (TME). For TME the emphasis lies on the combination with theory reasoners to be obtained by new compilation approach. \par Several theory-reasoning versions of connection calculi are defined and related to each other. In doing so, TME will be selected as a base to be developed further. The final versions are search-space restricted versions of total TME, partial TME and partial restart TME. These versions all are {\em answer\/}-complete, thus making TME interesting for logic programming and problem-solving applications. \par A theory reasoning system is only operable in combination with an (efficient) background reasoner for the theories of interest. Instead of hand-crafting respective background reasoners, a more general approach --- linearizing completion --- is proposed. Linearizing completion enables the {\em automatic\/} construction of background calculi suitable for TME-based theory reasoning systems from a wide range of axiomatically given theories, namely Horn theories. \par Technically, linearizing completion is a device for combining the unit-resulting strategy of resolution with a goal-oriented, linear strategy {\`a} la Prolog in a refutationally complete way. The method is presented in detail. \par Finally, an implementation extending the PTTP technique (Prolog based Technology Theorem Proving) towards theory reasoning is described, and the usefulness of the methods developed in this text will be experimentally demonstrated.", optannote = "" } @TechReport{ Baumgartner:Furbach:RMERefinements:TechRep:24:96, author = "Peter Baumgartner and Ulrich Furbach", title = "{Refinements for Restart Model Elimination}", institution = unikola, type = fbinformatik, address = unikolaaddress, year = "1996", number = "24--96", language = "english", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-24-96.ps.gz" , abstract = " We introduce and discuss a number of refinements for restart model elimination (RME). Most of these refinements are motivated by the use of RME as an interpreter for disjunctive logic programming. Especially head selection function, computation rule, strictness and independence of the goal clause are motivated by aiming at a procedural interpretation of clauses. Other refinements like regularity and early cancellation pruning are techniques to handle the tremendous search space. We discuss these techniques and investigate their compatibility. As a new result we give a proof of completeness for RME with early cancellation pruning; we furthermore show that this powerful refinement is compatibel with regularity tests. ", annote = "skip_html" } @TechReport{ Baumgartner:Furbach:CalculiForDLP:TechRep:13:96, author = "Peter Baumgartner and Ulrich Furbach", title = "{Calculi for Disjunctive Logic Programming}", institution = unikola, type = fbinformatik, address = unikolaaddress, year = "1996", number = "13--96", language = "english", url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-13-96.ps.gz" , keywords = "Disjunctive Logic Programming, Fixpoint Semantics, SLO, Theorem Proving", abstract = " We introduce a bottom-up and a top-down calculus for disjunctive logic programming (DLP). The bottom-up calculus, hyper tableaux, is depicted in its ground version and its relation to fixed point approaches from the literature is investigated. The top-down calculus, restart model elimination (RME), is presented as a sound and complete answer-computing mechanism for DLPs, and its relation to hyper tableaux is discussed. \\ In two aspect this represents an extension of SLD-resolution for Horn clause logic programming: RME {\em is\/} SLD-resolution when restricted to Horn clauses, and it has a direct counterpart to the immediate consequence operator for Horn clauses. Furthermore we discuss, that hyper tableaux can be seen as an extension of SLO-resolution.", annote = "skip_html" } @Misc{ Baumgartner:Furbach:HyperTableaux:Dagstuhl:96, optcrossref = "", optkey = "", author = "Peter Baumgartner and Ulrich Furbach", title = "{Hyper Tableaux. Part I: Proof Procedure and Model Generation}", howpublished = "Dagstuhl-Seminar Reports {\em Disjunctive logic programming and databases: Non-monotonic aspects\/}", year = "1996", optmonth = "", optnote = "", optannote = "" } @InCollection{ Baumgartner:Furbach:HyperTableauxAndDLP:DDLP:96, author = "Peter Baumgartner and Ulrich Furbach", title = "{Hyper Tableaux and Disjunctive Logic Programming}", booktitle = "ICLP 96 Workshop on Deductive Databases and Logic Programming", howpublished = "Workshop Deductive Databases and Logic Programming (DD\&LP'96) at {\em Joint International Conference and Symposium on Logic Programming\/}", year = "1996", url = "fix-jicslp96.pdf" , publisher = "GMD", opteditor = "", volume = "295", optnumber = "", series = "GMD Studien", abstract = " We introduce a bottom-up and a top-down calculus for disjunctive logic programming (DLP). The bottom-up calculus, hyper tableaux, is depicted in its ground version and its relation to fixed point approaches from the literature is investigated. The top-down calculus, restart model elimination (RME), is presented as a sound and complete answer-computing mechanism for DLPs, and its relation to hyper tableaux is discussed. \\ In two aspect this represents an extension of SLD-resolution for Horn clause logic programming: RME {\em is\/} SLD-resolution when restricted to Horn clauses, and it has a direct counterpart to the immediate consequence operator for Horn clauses. Furthermore we discuss, that hyper tableaux can be seen as an extension of SLO-resolution." } @Misc{ AIGROUP:MergingTPandLP:Poster:JICSLP:96, optcrossref = "", optkey = "", author = "Artificial Intelligence Research Group", title = "{Towards Merging Theorem Proving and Logic Programming Paradigms}", howpublished = "Proc. of the Poster Session at JICSLP '96, Editors: N. Fuchs and U. Geske", year = "1996", optmonth = "", note = "GMD Studien Nr. 296", optannote = "" } @InProceedings{ Baumgartner:Kuehn:Beckert:EHyperTableaux:DeduktionWS:96, author = "Peter Baumgartner and Bernhard Beckert and Michael K{\"u}hn", title = "{Extending Hyper Tableaux with Rigid $E$-Unification}", editor = "K. Prasser", number = "WV-96-09", series = "Internal Reports", booktitle = "Workshop Deduktion, 20.\ Jahrestagung f{\"u}r k{\"u}nstliche Intelligenz, Zusammenfassungen", year = 1996, organization = "Technische Universit{\"a}t Dresden", address = "Fakult{\"a}t Informatik, D01062 Dresden", url = "tableaux-dedtreff96.pdf" , abstract = "In \cite{Baumgartner:etal:HyperTableau:JELIA:96} we introduced a variant of clausal normal form tableaux called ``hyper tab\-leaux''. In the talk we well report about ongoing work on two improvements of the basic calculus. The first improvement deals with a shortcoming of the basic calculus, which is the need for ``purifying'' substitutions in disjunctions of positive literals. The second improvement is the extension with a dedicated inference rule for equality. We will use the completion-based method for mixed universal and rigid $E$-unification of \cite{Beckert:MixedUnification:94}. " } @TechReport{ Baumgartner:etal:TableauxDiagnosis:TechRep:23:96, author = "Peter Baumgartner and Peter Fr{\"o}hlich and Ulrich Furbach and Wolfgang Nejdl", title = "{Tableaux for Diagnosis Applications}", year = "1996", number = "23--96", language = "english", institution = unikola, type = fbinformatik, address = unikolaaddress, url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-23-96.ps.gz" , abstract = " In [Nejdl and Fr{\"o}hlich 96] a very efficient system for solving diagnosis tasks has been described, which is based on belief revision procedures and uses first order logic system descriptions. In this paper we demonstrate how such a system can be rigorously formalized from the viewpoint of deduction by using the calculus of hyper tableaux [Baumgartner et.al. 96]. The benefits of this approach are twofold: first, it gives us a clear logical description of the diagnosis task to be solved; second, as our experiments show, the approach is feasible in practice and thus serves as an example of a successful application of deduction techniques to real-world applications.", annote = "skip_html" } @Misc{ Baumgartner:Furbach:Stolzenburg:95b, author = {Peter Baumgartner and Ulrich Furbach and Frieder Stolzenburg}, title = {{Computing Answers and Logic Programming by Model Elimination Based Theorem Proving}}, year = {1995}, howpublished = {Proc. of the Workshop ``Automated Reasoning: Bridging the Gap between Theory and Practice''}, note = {Leeds, England}, optannote = { } } @TechReport{ Baumgartner:Schumann:RMESETHEO:TechRep:5:95, author = {Peter Baumgartner and Johann Schumann}, title = {{Implementing Restart Model Elimination and Theory Model Elimination on top of SETHEO}}, institution = unikola, type = fbinformatik, address = unikolaaddress, url = "http://www.uni-koblenz.de/fb4/publikationen/ gelbereihe/RR-5-95.ps.gz" , year = {1995}, number = {5--95}, abstract = {This paper presents an implementation for the efficient execution of Theory Model Elimination (TME), TME by Linearizing Completion, and Restart Model Elimination (RME) on top of the automated theorem prover {\small SETHEO}. These calculi allow for theory reasoning using a Model Elimination based theorem prover. They are described in detail and their major properties are shown. Then, a detailed description how TME by Linearizing Completion and RME can be implemented on top of {\small SETHEO}'s Abstract Machine (SAM) is given. Due to the flexibility of the Abstract Machine and its input language LOP, only simple transformations of the input formula are sufficient to obtain an efficient implementation. Only for RME, one machine-instruction of the SAM had to be modified slightly. We present results of experiments comparing plain {\small SETHEO} with an implementation of TME with PTTP (PROTEIN) and the {\small SETHEO} implementation presented here.} } @Article{ Baumgartner:Stolzenburg:DeduktionstreffenBericht:95, author = "Peter Baumgartner and Frieder Stolzenburg", title = "{Jahrestreffen der GI-Fachgruppe 1.2.1 Deduktion}", journal = {KI}, year = 1995, volume = 9, number = 6, pages = {80-81}, note = "Conference report" } @InProceedings{ Baumgartner:94b, author = {Peter Baumgartner and J{\"u}rgen Dix and Ulrich Furbach and Frieder Stolzenburg}, title = {{The Spectrum of Model Elimination based Theorem Proving}}, booktitle = {Informal Proceedings of the 11th Annual Meeting of the GI-Fachgruppe Deduktionssysteme}, organization = {TH Darmstadt}, year = {1994}, editor = {W. Bibel, C. Walther}, number = {AIDA-94-06}, series = {Research Report}, optannote = { } } @InProceedings{ Baumgartner:94c, author = {Peter Baumgartner}, title = {{A Transformation Technique to Combine the Linear and the Unit-Resulting Restrictions}}, booktitle = {Proceedings of the Eight International Symposium on Methodologies for Intelligent Systems}, organization = {Oak Ridge National Laboratory}, year = {1994}, address = {Charlotte, N.C, USA}, optannote = { } } @InProceedings{ Baumgartner:Furbach:94c, author = {Peter Baumgartner and Ulrich Furbach}, title = {{Model Elimination without Contrapositives and its Application to PTTP}}, booktitle = {TABLEAUX-'94 Workshop}, organization = {Imperial College}, year = {1994}, editor = {Broda D'Agostino Gor{\'e} Johnson Reeves}, number = {TR-94/5}, series = {Technical Report}, optannote = { } } @InProceedings{ Baumgartner:Furbach:94d, author = {Peter Baumgartner and Ulrich Furbach}, title = {{Lineare Vervollst{\"a}ndigung f{\"u}r die Behandlung von Horntheorien}}, booktitle = {DFG-Colloquium ``Deduction''}, organization = {Technische Hochschule Darmstadt}, year = {1994}, number = {AIDA-94-02}, series = {Research Report}, optannote = { } } @Misc{ Baumgartner:Furbach:94e, author = {Peter Baumgartner and Ulrich Furbach}, title = {{The Spectrum of Model Elimination Based Theorem Proving}}, year = {1994}, howpublished = {Proc. of the Workshop ``Automated Reasoning: Bridging the Gap between Theory and Practice''}, note = {Leeds, England}, optannote = { } } @InProceedings{ Baumgartner:Furbach:Stolzenburg:94, author = {Peter Baumgartner and Ulrich Furbach and Frieder Stolzenburg}, title = {{Applications of Theory Reasoning in Model Elimination}}, booktitle = {Theory Reasoning in Automated Deduction}, year = {1994}, editor = {Peter Baumgartner and H.-J. B{\"u}rckert and H. Comon and Ulrich Furbach and Mark Stickel}, series = {CADE-12 Workshop Proceedings}, optannote = { } } @Proceedings{ Baumgartner:etal:94, title = {{Theory Reasoning in Automated Deduction}}, organization = {INRIA, Lorraine}, year = {1994}, editor = {Peter Baumgartner, H.-J. B{\"u}rckert and H. Comon}, note = {Technical Report}, series = {12th International Conference on Automated Deduction, Workshop}, optannote = { } } @TechReport{ Stolzenburg:Baumgartner:CME:TechRep:10:94, author = {Frieder Stolzenburg and Peter Baumgartner}, title = {{Constraint Model Elimination and a PTTP-Implementation}}, institution = unikola, type = fbinformatik, address = unikolaaddress, url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-10-94.ps.gz" , year = "1994", number = "10/94", abstract = "In constraint logic programming, proof procedures for {\em Horn\/} clauses are enhanced with an interface to efficient constraint solvers. The question arises whether it is possible to incorporate constraint processing into general, non-Horn theorem proving calculi. In this paper, a positive answer to this question will be given. A framework for a new calculus is introduced which combines model elimination with constraint solving, following the lines of B{\"u}rckert (1991). A prototype system has been implemented rapidly by only combining a PROLOG technology implementation of model elimination and PROLOG with constraints. Some example studies, e.g. taxonomic reasoning, show the advantages and some problems with this procedure. ", annote = "skip_html" } @InProceedings{ Stolzenburg:Baumgartner:94b, author = {Frieder Stolzenburg and Peter Baumgartner}, title = {{Constraint Model Elimination and a PTTP-Implementation}}, booktitle = {Workshop on Constraint Languages and their Use in Problem Modelling --- International Logic Programming Symposium}, year = {1994}, editor = {J. Jourdan, P. Lim, R. Yap}, optannote = { } } @TechReport{ Baumgartner:93a, author = {Peter Baumgartner}, title = {{Refinements of Theory Model Elimination and a Variant without Contrapositives}}, institution = unikola, type = fbinformatik, address = unikolaaddress, year = {1993}, number = {8/93}, optnote = {(Short version in {\em Proc. ECAI 94, 1994, Wiley\/})} } @TechReport{ Baumgartner:TPTPWorkshop:7:93, author = "Peter Baumgartner\quad(Editor)", title = "{Workshop PTTP-basiertes Theorembeweisen}", year = "1993", number = "7--93", language = "german", institution = unikola, type = fbinformatik, address = unikolaaddress } @InProceedings{ Baumgartner:93c, author = {Peter Baumgartner}, title = {{Combining Model Elimination and Unit-Resulting Resolution}}, booktitle = {Proc. Tableau-Workshop}, year = {1993}, address = {Marseille}, note = {MPI-Report I-93-213}, optpublisher = {Max Planck Institute for Computer Science} } @InProceedings{ Baumgartner:92d, author = {Peter Baumgartner}, title = {{A Model Elimination Calculus with Built-In Theories}}, booktitle = {Theorem Proving with Analytic Tableaux and Related Methods}, year = {1992}, editor = {{Fronh{\"o}fer, H{\"a}hnle, K{\"a}ufl}}, number = {8/92}, series = {Technical Report}, optannote = { } } @InProceedings{ Baumgartner:92b, author = {Peter Baumgartner}, title = {{Partial Unification for Ordered Theory Resolution}}, booktitle = {6th International Workshop on Unification}, organization = {IBFI Dagstuhl}, year = {1992}, editor = {F. Baader and J. Siekmann and W. Snyder}, note = {Dagstuhl Seminar Report 42} } @InProceedings{ Baumgartner:Furbach:92a, author = {Peter Baumgartner}, title = {{Consolution as a Framework for Comparing Calculi}}, booktitle = {Theorem Proving with Analytic Tableaux and Related Methods}, year = {1992}, editor = {{Fronh{\"o}fer, H{\"a}hnle, K{\"a}ufl}}, number = {8/92}, series = {Technical Report}, optannote = { } } @TechReport{ Baumgartner:Furbach:Petermann:UnifiedApproachTheoryReasoning:TechRep:15:92, author = {Peter Baumgartner and Ulrich Furbach and Uwe Petermann}, title = {{A Unified Approach to Theory Reasoning}}, institution = unikola, type = fbinformatik, address = unikolaaddress, year = {1992}, url = "thover.pdf" , abstract = "{\em Theory reasoning} is a kind of two-level reasoning in automated theorem proving, where the knowledge of a given domain or theory is separated and treated by special purpose inference rules. We define a classification for the various approaches for theory reasoning which is based on the syntactic concepts of {\em literal level --- term level --- variable level\/}. The main part is a review of theory extensions of common calculi (resolution, model elimination and a connection method). In order to see the relationships among these calculi, we define a super-calculus called {\em theory consolution\/}. Completeness of the various theory calculi is proven. Finally, due to its relevance in automated reasoning, we describe current ways of equality handling.", number = "15/92" } @TechReport{ Baumgartner:90a, author = {Peter Baumgartner}, title = {{Modelling Software Reuse with Predicate Logic}}, institution = unikola, type = fbinformatik, address = unikolaaddress, year = {1990}, number = {12/90} } @TechReport{ Baumgartner:etal:90, author = {Peter Baumgartner and S. Meggendorfer and Z. Qiu}, title = {{Software Specification Methods from the Viewpoint of Reusability}}, institution = {Technische Universit{\"a}t M{\"u}nchen}, year = {1990}, month = {July}, number = {FKI--133--90}, type = {AI research report}, optnote = { } } @MastersThesis{ Baumgartner:88, author = {Peter Baumgartner}, title = {{Theorie und Implementierung eines kombinierten logischen und funktionalen Programmiersystems}}, year = {1988}, school = {{Technische Universit{\"a}t M{\"u}nchen}}, note = {(In German)}, optannote = { } } @Proceedings{ TABLEAUX:95, booktitle = {Theorem Proving with Analytic Tableaux and Related Methods}, title = {Theorem Proving with Analytic Tableaux and Related Methods}, year = {1995}, editor = {Peter Baumgartner and Reiner H{\"a}hnle and J. Posegga}, publisher = {Springer}, volume = {918}, series = lnai } @Proceedings{ TABLEAUX:97, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods}, title = {Automated Reasoning with Analytic Tableaux and Related Methods}, year = {1997}, editor = {Didier Galmiche}, publisher = {Springer}, volume = {1227}, series = lnai, optannote = { } } @Proceedings{ TABLEAUX:98, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods}, title = {Automated Reasoning with Analytic Tableaux and Related Methods}, year = {1998}, editor = {Harry de Swaart}, publisher = {Springer}, volume = {1397}, series = lnai, optannote = { } } @Proceedings{ TABLEAUX:99, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods}, title = {Automated Reasoning with Analytic Tableaux and Related Methods}, year = {1999}, editor = {Neil Murray}, publisher = {Springer}, volume = {1617}, series = lnai } @Proceedings{ IJCAI:95, booktitle = {14th International Joint Conference on Artificial Intelligence (IJCAI 95)}, year = "1997", publisher = {Morgan Kaufmann}, address = "Montreal" } @Proceedings{ IJCAI:97, booktitle = {15th International Joint Conference on Artificial Intelligence (IJCAI 97)}, editor = {M. E. Pollack}, year = "1997", publisher = {Morgan Kaufmann}, address = "Nagoya" } @Proceedings{ CADE:99, booktitle = {CADE-16 -- The 16th International Conference on Automated Deduction}, editor = {Harald Ganzinger}, year = {1999}, volume = {1632}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, title = {Automated Deduction -- CADE-16}, address = {Trento, Italy} } @Proceedings{ CADE:05, booktitle = {CADE-20 -- The 20th International Conference on Automated Deduction}, editor = {Robert Nieuwenhuis}, year = {2005}, volume = {3632}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, title = {Automated Deduction -- CADE-20} } @Proceedings{ CADE:09, booktitle = {CADE-22 -- The 22nd International Conference on Automated Deduction}, editor = {Renate Schmidt}, year = {2009}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, volume = {5663}, title = {Automated Deduction -- CADE-22} } @Proceedings{ CADE:07, booktitle = {CADE-21 -- The 21st International Conference on Automated Deduction}, editor = {Frank Pfenning}, year = {2007}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, volume = {4603}, title = {Automated Deduction -- CADE-21} } @Proceedings{ CADE:00, booktitle = {CADE-17 -- The 17th International Conference on Automated Deduction}, editor = {David McAllester}, year = {2000}, volume = {1831}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, title = {Automated Deduction -- CADE-17} } @Proceedings{ CADE:03, booktitle = {CADE-19 -- The 19th International Conference on Automated Deduction}, editor = {Franz Baader}, year = {2003}, volume = {2741}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, title = {Automated Deduction -- CADE-19} } @Proceedings{ Baumgartner:Zhang:FirstOrderTheoremProving:JSC:01, title = {First-Order Theorem Proving}, year = {2003}, optkey = {}, editor = {Peter Baumgartner and Hantao Zhang}, volume = {36}, number = {1-2}, series = {Special issue of the Journal of Symbolic Computation}, optaddress = {}, optmonth = {}, optorganization={}, publisher = {Academic Press}, optannote = {} } @Proceedings{ CL2000:00, booktitle = {Computational Logic -- CL 2000}, editor = {John Lloyd and Veronica Dahl and Ulrich Furbach and Manfred Kerber and Kung-Kiu Lau and Catuscia Palamidessi and Luis Moniz Pereira and Yehoshua Sagiv and Peter J. Stuckey}, year = {2000}, volume = {1861}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, title = {Computational Logic -- CL 2000} } @Proceedings{ Baumgartner:etal:ModelComputation:WS:CADE:00, title = {CADE-17 Workshop on Model Computation - Principles, Algorithms, Applications}, booktitle = {CADE-17 Workshop on Model Computation - Principles, Algorithms, Applications}, year = {2000}, note = "http://www.uni-koblenz.de/{\textasciitilde}peter/CADE17-WS-MODELS/" , url = "http://www.uni-koblenz.de/~peter/CADE17-WS-MODELS/", editor = {Peter Baumgartner and Chris Ferm{\"u}ller and Nicolas Peltier and Hantao Zhang} } @Proceedings{ Ahrendt:etal:DisprovingAndPDPAR:ENTCS:05, title = {{S}elected {P}apers from the {W}orkshops on {D}isproving and the {S}econd {I}nternational {W}orkshop on {P}ragmatics of {D}ecision {P}rocedures ({PDPAR} 2004)}, booktitle = {{S}elected {P}apers from the {W}orkshops on {D}isproving and the {S}econd {I}nternational {W}orkshop on {P}ragmatics of {D}ecision {P}rocedures ({PDPAR} 2004)}, editor = {Wolfgang Ahrendt and Peter Baumgartner and Hans de Nivelle and Silvio Ranise and Cesare Tinelli}, year = {2005}, volume = {125}, number = {3}, pages = {1-164}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, url = "http://www.sciencedirect.com/science?_ob=IssueURL&_tockey=%23TOC%2313109%232005%23998749996%23601031%23FLP%23display%23Volume_125,_Issue_3,_Pages_1-164_(18_July_2005)%2BMSelected_Papers_from_the_Workshops_on_Disproving_and_the_Second_International_Workshop_on_Pragmatics_of_Decision_Procedures_(PDPAR_2004)%2BM2004%2BMEdited_by_W._Ahrendt,_P._Baumgartner,_H._de_Nivelle,_S._Ranise_and_C._Tinelli%23tagged%23Volume%23first%3D125%23Issue%23first%3D3%23date%23(18_July_2005)%23specissname%23Selected_Papers_from_the_Workshops_on_Disproving_and_the_Second_International_Workshop_on_Pragmatics_of_Decision_Procedures_(PDPAR_2004)%23specissdate%232004%23specisseditor%23Edited_by_W._Ahrendt,_P._Baumgartner,_H._de_Nivelle,_S._Ranise_and_C._Tinelli%23&_auth=y&view=c&_acct=C000004638&_version=1&_urlVersion=0&_userid=43521&md5=9f61c21be3c35831ab97d6d162981c53" } @Proceedings{ Ahrendt:etal:Disproving:IJCAR-WS:2006, title = {Third Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability (DISPROVING'06)}, booktitle = {Third Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability (DISPROVING'06)}, year = {2006}, optkey = {}, editor = {Wolfgang Ahrendt and Peter Baumgartner and Hans de Nivelle}, optvolume = {}, optnumber = {}, optseries = {}, address = {Seattle}, optmonth = {}, optorganization={}, optpublisher = {}, note = {Workshop at IJCAR'06}, optannote = {} } @Proceedings{ Baumgartner:etal:ProblemSolvingMethodologies:WS:CADE:98, title = {CADE-15 Workshop on Problem-solving Methodologies with Automated Deduction}, booktitle = {CADE-15 Workshop on Problem-solving Methodologies with Automated Deduction}, year = {1998}, note = "http://www.uni-koblenz.de/{\textasciitilde}peter/cade-15-ws/" , optkey = {}, editor = {Peter Baumgartner and Ulrich Furbach and Michael Kohlhase and William McCune and Wolfgang Reif and Mark Stickel and Tom{\`a}s Uribe}, optvolume = {}, optnumber = {}, optseries = {}, optaddress = {}, optmonth = {}, optorganization={}, optpublisher = {}, optnote = {}, optannote = {} } @Proceedings{ ILPS:97, booktitle = {Logic Programming - Proceedings of the 1997 International Symposium}, editor = {Jan Maluszynski}, year = {1997}, publisher = {The MIT Press}, title = {Logic Programming - Proceedings of the 1997 International Symposium}, address = {Port Jefferson, New York} } @Proceedings{ Bibel:Schmitt:DFGBook:98, title = "Automated Deduction. A basis for applications", booktitle = "Automated Deduction. A Basis for Applications", year = "1998", optcrossref = "", optkey = "", editor = "Wolfgang Bibel and Peter H. Schmitt", optvolume = "", optnumber = "", optseries = "", publisher = "Kluwer Academic Publishers", optorganization="", optaddress = "", optmonth = "", optannote = "" }