peter-2009.bib

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

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

@inproceedings{Baumgartner:Slaney:ConstraintModellingChallenge:FTP:2009,
  author = {Peter Baumgartner and John Slaney},
  title = {Constraint Modelling: A Challenge for Automated Reasoning},
  optcrossref = {},
  optkey = {},
  booktitle = {Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)},
  era = {B},
  pages = {4-18},
  editor = {Nicolas Peltier and Viorica Sofronie-Stokkermans},
  volume = {556},
  optnumber = {},
  series = {Workshop Proceedings},
  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 = {CEUR},
  optnote = {},
  isbn = {1613-0073},
  optannote = {}
}

@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 = {},
  era = {A},
  series = {LNAI},
  optaddress = {},
  month = {July},
  doi = {10.1007/978-3-642-02716-1\_7},
  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.},
  era = {A},
  url = {MESUP-CADE.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},
  era = {A},
  pages = {58-74},
  month = {March},
  doi = {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}
}

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