peter-2014.bib

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

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

@inproceedings{Baumgartner:Bax:Waldmann:FiniteQuantificationHSP:IJCAR:2014,
  author = {Peter Baumgartner and Joshua Bax and Uwe Waldmann},
  title = {Finite Quantification in Hierarchic Theorem Proving},
  optcrossref = {},
  optkey = {},
  booktitle = {IJCAR 2014},
  year = {2014},
  editor = {S. Demri and D. Kapur and C. Weidenbach},
  volume = {8562},
  optnumber = {},
  series = {LNAI},
  pages = {152--167},
  url = {finite-quantification-IJCAR-2014.pdf},
  optmonth = {},
  address = {Vienna},
  optorganization = {},
  publisher = {Springer Switzerland},
  abstract = {
	Many applications of automated deduction require reasoning in
	first-order logic modulo background theories, in particular some
	form of integer arithmetic.  A major unsolved research challenge
	is to design theorem provers that are ``reasonably complete'' even
	in the presence of free function symbols ranging into a
	background theory sort. In this paper we consider the case when
	all variables occurring below such function symbols are
	quantified over a finite subset of their domains.  We present a
	non-naive decision procedure for background theories extended
	this way on top of black-box decision procedures for the
	EA-fragment of the background theory.  In its core, it employs a
	model-guided instantiation strategy for obtaining pure
	background formulas that are equi-satisfiable with the original
	formula.  Unlike traditional finite model finders, it avoids
	exhaustive instantiation and, hence, is expected to scale better
	with the size of the domains.  Our main results in this paper are
	a correctness proof and first experimental results.}
}

@article{Baumgartner:ModelEvolutionBasedTheoremProving:IEEE:2014,
  author = {Peter Baumgartner},
  title = {Model Evolution Based Theorem Proving},
  journal = {IEEE Intelligent Systems},
  year = {2014},
  optkey = {},
  volume = {29},
  number = {1},
  pages = {4--10},
  month = {Jan.--Feb.},
  optnote = {},
  optannote = {},
  url = {MEBasedTheoremProving.pdf},
  doi = {10.1109/MIS.2013.124},
  copyright = {Copyright IEEE, \url{http://www.ieee.org}}
}

@inproceedings{Baumgartner:Waldmann:HSPBeagle:Dagstuhl:2014,
  author = {Peter Baumgartner and Uwe Waldmann},
  title = {Hierarchic superposition with weak abstraction and the Beagle theorem prover},
  url = {http://drops.dagstuhl.de/opus/volltexte/2014/4425},
  booktitle = {{Deduction and Arithmetic (Dagstuhl Seminar 13411)}},
  journal = {Dagstuhl Reports},
  issn = {2192-5283},
  year = {2014},
  volume = {3},
  number = {10},
  editor = {Nikolaj Bjorner and Reiner H{\"a}hnle and Tobias Nipkow and Christoph Weidenbach},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address = {Dagstuhl, Germany},
  urn = {urn:nbn:de:0030-drops-44250},
  doi = {http://dx.doi.org/10.4230/DagRep.3.10.1},
  abstract = {Many applications of automated deduction require reasoning
                  in first-order logic modulo background theories, in
                  particular some form of integer arithmetic. A major unsolved
                  research challenge is to design theorem provers that are
                  "reasonably complete" even in the presence of free function
                  symbols ranging into a background theory sort. The earlier
                  hierarchic superposition calculus of Bachmair, Ganzinger,
                  and Waldmann already supports such symbols, but, not
                  optimally. We have devised a new calculus, hierarchic
                  superposition with weak abstraction, which rectifies this
                  situation by introducing a novel form of clause abstraction,
                  a core component in the hierarchic superposition calculus
                  for transforming clauses into a form needed for internal
                  operation. Additionally, it includes a definition rule
                  that is generally useful to find refutations more often, and,
                  specifically, gives completeness for the clause logic
                  fragment where all background-sorted terms are ground.  The
                  talk provides an overview of the calculus, its
                  implementation in the Beagle theorem prover and experiments
                  with it.  }
}