peter-2020.bib

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

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

@inproceedings{Baumgartner:PossibleModelsSpringer:IJCAR:2020,
  author = {Peter Baumgartner},
  title = {{Possible Models Computation and Revision -- A Practical Approach}},
  optcrossref = {},
  optkey = {},
  booktitle = {International Joint Conference on Automated Reasoning},
  year = {2020},
  editor = {N. Peltier and V. Sofronie-Stokkermans},
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {337--355},
  volume = {12166},
  optnumber = {},
  series = {LNAI},
  url = {possible-models-IJCAR-2020.pdf},
  note = {doi 10.1007/978-3-030-79876-5\_34},
  optorganization = {},
  copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}},
  abstract = {This paper describes a method of computing plausible states of a system as a logical model.
  The problem of analyzing state-based systems as they evolve over time has been
  studied widely in the automated reasoning community (and others). This paper
  proposes a specific approach, one that is tailored to
  situational awareness applications. The main contribution is a calculus for a novel specification
  language that is built around disjunctive logic programming under a possible models
  semantics, stratification in terms of event times, default negation, and a model
  revision operator for dealing with incomplete or erroneous events -- a typical problem
  in realistic applications.  The paper proves the calculus correct wrt.\ a formal
  semantics of the specification language and it describes the calculus' implementation
  via embedding in Scala.  This enables immediate access to rich data structures
  and external systems, which is important in practice.}
}

@article{Baumgartner:Schmidt:BUMGEnhanced:JAR:2019,
  author = {Peter Baumgartner and Renate Schmidt},
  title = {Blocking and Other Enhancements for Bottom-Up Model Generation Methods},
  journal = {Journal of Automated Reasoning},
  year = {2020},
  volume = {64},
  pages = {197--251},
  url = {https://rdcu.be/bo9Tz},
  publisher = {Springer},
  doi = {10.1007/s10817-019-09515-1},
  era = {A},
  abstract = {Model generation is a problem complementary to theorem proving
 and is important for fault analysis and debugging of formal
 specifications of security protocols, programs and terminological
 definitions, for example.  This paper discusses several ways of
 enhancing the paradigm of bottom-up model generation, with the
 two main contributions being a new range-restriction
 transformation and generalized blocking techniques.  The
 range-restriction transformation refines existing transformations
 to range-restricted clauses by carefully limiting the creation of
 domain terms.  The blocking techniques are based on simple
 transformations of the input set together with standard equality
 reasoning and redundancy elimination techniques, and allow for
 finding small, finite models.  All possible combinations of the
 introduced techniques and a classical range-restriction technique
 were tested on the clausal problems of the TPTP Version 6.0.0
 with an implementation based on the SPASS theorem prover using a
 hyperresolution-like refinement.  Unrestricted domain blocking
 gave best results for satisfiable problems, showing that it is an
 indispensable technique for bottom-up model generation methods,
 that yields good results in combination with both new and
 classical range-restricting transformations.  Limiting the
 creation of terms during the inference process by using the new
 range-restricting transformation has paid off, especially when
 using it together with a shifting transformation.  The
 experimental results also show that classical range restriction
 with unrestricted blocking provides a useful complementary
 method.  Overall, the results show bottom-up model generation
 methods are good for disproving theorems and generating models
 for satisfiable problems, but less efficient for unsatisfiable
 problems.}
}