peter-2008.bib

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

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

@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 = {Lecture Notes in Artificial Intelligence},
  era = {A},
  url = {MELIA.pdf},
  month = {November},
  publisher = {Springer},
  doi = {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},
  era = {A*},
  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 = {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 = {},
  era = {A},
  publisher = {Springer},
  doi = {10.1007/978-3-540-71070-7},
  optnote = {},
  optannote = {}
}