peter-2003.bib

@comment{{This file has been generated by bib2bib 1.95}}
@comment{{Command line: bib2bib -c 'year=2003 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-2003.bib -oc peter-2003.cite peter.bib}}
@article{Baumgartner:Furbach:DeductionPersonalizedDocuments:AnnalsMathAI:03,
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{Automated Deduction Techniques for the Management of
		  Personalized Documents}},
  journal = {Annals of Mathematics and Artificial Intelligence --
		  Special Issue on Mathematical Knowledge Management},
  year = {2003},
  optkey = {},
  publisher = {Kluwer Academic Publishers},
  volume = {38},
  number = {1},
  optpages = {},
  optmonth = {},
  url = {MKMLinzJournalFinal.pdf},
  abstract = { This work is about a ``real-world'' application of
		  automated deduction. The application is the management of
		  documents (such as mathematical textbooks) as they occur in
		  a readily available tool. In this ``Slicing Information
		  Technology tool'', documents are decomposed (``sliced'')
		  into small units. A particular application task is to
		  assemble a new document from such units in a selective way,
		  based on the user's current interest and knowledge. \par It
		  is argued that this task can be naturally expressed through
		  logic, and that automated deduction technology can be
		  exploited for solving it. More precisely, we rely on
		  first-order clausal logic with some default negation
		  principle, and we propose a model computation theorem
		  prover as a suitable deduction mechanism. \par Beyond
		  solving the task at hand as such, with this work we
		  contribute to the quest for arguments in favor of automated
		  deduction techniques in the ``real world''. Also, we argue
		  why we think that automated deduction techniques are the
		  best choice here.},
  era = {C},
  optannote = {}
}
@inproceedings{Baumgartner:etal:LivingBooks:WI:2003,
  author = {Peter Baumgartner and Ulrich Furbach and Margret
		  Gro{\ss}-Hardt},
  title = {Living Books},
  booktitle = {Wirtschaftsinformatik 2003},
  optcrossref = {},
  optkey = {},
  pages = {693--706},
  year = {2003},
  editor = {Wolfgang Uhr and Werner Esswein and Eric Schoop},
  volume = {1},
  optnumber = {},
  optseries = {},
  optaddress = {},
  optmonth = {},
  optorganization = {},
  publisher = {Physica-Verlag},
  optannote = {}
}
@inproceedings{Baumgartner:Tinelli:ModelEvolutionCalculus:CADE:2003,
  author = {Peter Baumgartner and Cesare Tinelli},
  title = {{The Model Evolution Calculus}},
  crossref = {CADE:03},
  pages = {350-364},
  era = {A},
  url = {BaumgartnerTinelli-CADE-19.pdf},
  abstract = {The DPLL procedure, due to Davis, Putnam, Logemann, and
		  Loveland, 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. \par The recent FDPLL
		  calculus by Baumgartner was the first successful attempt to
		  lift the procedure to the first-order level without
		  recurring 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\/},
		  one of FDPLL's optimizations, and so has the potential of
		  leading to much faster implementations.}
}
@inproceedings{Baumgartner:Etal:LivingBook:CADE:2003,
  author = {Peter Baumgartner and Ulrich Furbach and Margret
		  Gross-Hardt and Alex Sinner},
  title = {{\ttfamily\bfseries 'Living Book' :- 'Deduction',
		  'Slicing', 'Interaction'.} -- System Description},
  crossref = {CADE:03},
  era = {A},
  year = {2003},
  pages = {284--288},
  abstract = {This system description is about a real-world application
		  of automated deduction. The system that we describe -- The
		  Living Book -- is a tool for the management of personalized
		  teaching material. The main goal of the Living Book system
		  is to support the active, explorative and self-determined
		  learning in lectures, tutorials and self study. It includes
		  a course on 'logic for computer scientists' with a uniform
		  access to various tools like theorem provers and an
		  interactive tableau editor\footnote{This work is sponsored
		  by EU IST-Grant TRIAL-SOLUTION and Bmbf-Grant In2Math.}.
		  This course is routinely used within teaching undergraduate
		  courses at our university.}
}
@inproceedings{Baumgartner:etal:KRHyperInsideModelBasedDeductionApplications:CADE-19-WS:2003,
  author = {Peter Baumgartner and Ulrich Furbach and Margret
		  Gross-Hardt and Thomas Kleemann and Christoph Wernhard},
  title = {KRHyper Inside --- Model Based Deduction in Applications},
  booktitle = {Proc.\ CADE-19 Workshop on Novel Applications of Deduction
		  Systems},
  optcrossref = {},
  optkey = {},
  optpages = {},
  year = {2003},
  url = {novel.pdf},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  optmonth = {},
  optorganization = {},
  optpublisher = {},
  optnote = {},
  optannote = {},
  abstract = {Three real world applications are depicted which all have
		  in common, that their core component is a full first order
		  theorem prover, based on the hyper tableau calculus. These
		  applications concern information retrieval in electronic
		  publishing, the integration of description logics with
		  other knowledge representation techniques and XML query
		  processing.}
}
@techreport{baumgartner:tinelli:1:2003,
  author = {Peter Baumgartner and Cesare Tinelli},
  title = {{The Model Evolution Calculus}},
  institution = {{Universit{\"a}t Koblenz-Landau}},
  year = {{2003}},
  type = {Fachberichte Informatik},
  number = {1--2003},
  language = {english},
  address = {Universit{\"a}t Koblenz-Landau, Institut f{\"u}r
		  Informatik, Rheinau 1, D-56075 Koblenz},
  url = {http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-1-2003.pdf},
  abstract = {The DPLL procedure, due to Davis, Putnam, Logemann, and
		  Loveland, 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. \par The recent FDPLL
		  calculus by Baumgartner was the first successful attempt to
		  lift the procedure to the first-order level without
		  recurring 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\/},
		  one of FDPLL's optimizations, and so has the potential of
		  leading to much faster implementations.}
}
@proceedings{CADE:03,
  booktitle = {CADE-19 -- The 19th International Conference on Automated
		  Deduction},
  editor = {Franz Baader},
  year = {2003},
  volume = {2741},
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  title = {Automated Deduction -- CADE-19}
}
@proceedings{Baumgartner:Zhang:FirstOrderTheoremProving:JSC:01,
  title = {First-Order Theorem Proving},
  year = {2003},
  optkey = {},
  editor = {Peter Baumgartner and Hantao Zhang},
  volume = {36},
  number = {1-2},
  series = {Special issue of the Journal of Symbolic Computation},
  optaddress = {},
  optmonth = {},
  optorganization = {},
  publisher = {Academic Press},
  optannote = {}
}