peter-2012.bib

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

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

@article{Barnes:etal:AIatNICTA:AIMagazine:2012,
  author = {Nick Barnes and
               Peter Baumgartner and
               Tib{\'e}rio S. Caetano and
               Hugh F. Durrant-Whyte and
               Gerwin Klein and
               Penelope Sanderson and
               Abdul Sattar and
               Peter J. Stuckey and
               Sylvie Thi{\'e}baux and
               Pascal Van Hentenryck and
               Toby Walsh},
  title = {{AI@NICTA}},
  journal = {AI Magazine},
  volume = {33},
  number = {3},
  year = {2012},
  pages = {115-},
  url = {http://www.aaai.org/ojs/index.php/aimagazine/article/view/2430}
}

@article{Bauer:etal:reasoning-BP:draft,
  author = {Andreas Klaus Bauer and
               Peter Baumgartner and
               Michael Norrish},
  title = {Reasoning with Data-Centric Business Processes},
  journal = {CoRR},
  volume = {abs/1207.2461},
  year = {2012},
  url = {http://arxiv.org/abs/1207.2461},
  abstract = {We describe an approach to modelling and reasoning about
    data-centric business processes and present a form of general
    model checking.  Our technique extends existing approaches, which
    explore systems only from concrete initial states.
    \par
    Specifically, we model business processes in terms of smaller
    fragments, whose possible interactions are constrained by
    first-order logic formulae.  In turn, process fragments are
    connected graphs annotated with instructions to modify data.
    Correctness properties concerning the evolution of data with
    respect to processes can be stated in a first-order
    branching-time logic over built-in theories, such as linear
    integer arithmetic, records and arrays.
    \par
    Solving general model checking problems over this logic is
    considerably harder than model checking when a concrete initial
    state is given.  To this end, we present a tableau procedure that
    reduces these model checking problems to first-order logic over
    arithmetic. The resulting proof obligations are passed on to
    appropriate ``off-the-shelf'' theorem provers.  We also detail our
    modelling approach, describe the reasoning components and report
    on first experiments.}
}

@inproceedings{Sutcliffe:etal:TPTP-TFFA:LPAR:2012,
  author = {Geoff Sutcliffe and Stephan Schulz and Koen Claessen and Peter Baumgartner},
  title = {{The TPTP Typed First-order Form with Arithmetic}},
  booktitle = {Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18)},
  year = {2012},
  editor = {Nikolaj Bj{\o}rner and Andrei Voronkov},
  series = {Lecture Notes in Artificial Intelligence},
  era = {A},
  url = {TFFArith.pdf},
  volume = {7180},
  publisher = {Springer},
  copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}},
  abstract = {The TPTP World is a well established infrastructure supporting research,
development, and deployment of Automated Theorem Proving systems.
Recently, the TPTP World has been extended to include a typed first-order
logic, which in turn has enabled the integration of arithmetic.
This paper describes these developments.}
}

@article{Baumgartner:Pelzer:Tinelli:MEERevised:JSC:2012,
  author = {Peter Baumgartner and Bj\"orn Pelzer and Cesare Tinelli},
  title = {Model Evolution with Equality -- Revised and Implemented},
  journal = {Journal of Symbolic Computation},
  url = {MEE-revised-final.pdf},
  doi = {10.1016/j.jsc.2011.12.031},
  copyright = {Copyright Elsevier \url{http://www.elsevier.com/}},
  year = {2012},
  optkey = {},
  volume = {47},
  number = {9},
  pages = {1011-1045},
  month = {September},
  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 superposition 
  inference rule, where equations used for superposition
  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 theoretical
  result is the correctness of the MEE calculus in the presence of
  very general redundancy elimination criteria. 
  We also describe our implementation of the calculus, the
  E-Darwin system, and we report on practical experiments with
  it on the TPTP problems library.},
  era = {A}
}