peter-2003.bib
@comment{{This file has been generated by bib2bib 1.99}}
@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 = {}
}