peter-2006.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bib2bib -c 'year=2006 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-2006.bib -oc peter-2006.cite peter.bib}}

@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},
  era = {A},
  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},
  era = {A},
  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: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},
  era = {C},
  year = {2006},
  editor = {Stephan Schulz and Geoff Sutcliffe and Tanel Tammet},
  volume = 15,
  number = 1,
  pages = {21--52},
  url = {implementing-ME-published.pdf}
}

@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 = {}
}