cw.bib
@inproceedings{Wernhard:2010:LP,
author = {Christoph Wernhard},
title = {Circumscription and Projection as Primitives of Logic Programming},
booktitle = {Technical Communications of the 26th International
Conference on Logic Programming, ICLP'10},
year = {2010},
volume = {7},
editor = {M.~Hermenegildo and T.~Schaub},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in
Informatics (LIPIcs)},
address = {Dagstuhl, Germany},
isbn = {978-3-939897-17-0},
issn = {1868-8969},
url = {http://drops.dagstuhl.de/opus/volltexte/2010/2598/},
doi = {10.4230/LIPIcs.ICLP.2010.281},
note = {(Extended version:
\url{http://cs.christophwernhard.com/papers/logprog2010extended.pdf})},
abstract = {We pursue a representation of logic programs as classical
first-order sentences. Different semantics for logic
programs can then be expressed by the way in which they are
wrapped into - semantically defined - operators for
circumscription and projection. (Projection is a
generalization of second-order quantification.) We
demonstrate this for the stable model semantics, Clark's
completion and a three-valued semantics based on the Fitting
operator. To represent the latter, we utilize the polarity
sensitiveness of projection, in contrast to second-order
quantification, and a variant of circumscription that allows
to express predicate minimization in parallel with
maximization. In accord with the aim of an integrated view
on different logic-based representation techniques, the
material is worked out on the basis of first-order logic
with a Herbrand semantics.}
}
@inproceedings{Wernhard:2009:ProjectionCircumscription,
author = {Christoph Wernhard},
title = {Literal Projection and Circumscription},
booktitle = {Proceedings of the 7th
International Workshop on First-Order Theorem Proving, FTP'09},
series = {CEUR Workshop Proceedings},
volume = {556},
year = {2010},
url = {http://ceur-ws.org/Vol-556},
editor = {Nicolas Peltier and Viorica Sofronie-Stokkermans},
note = {(Extended version:
\url{http://cs.christophwernhard.com/papers/projection-circumscription.pdf})},
abstract = {We develop a formal framework intended as a preliminary step for
a single knowledge representation system that provides
different representation techniques in a unified way. In
particular we consider first-order logic extended by
techniques for second-order quantifier elimination and
non-monotonic reasoning. In this paper two independent
results are developed. The background for the first result
is literal projection, a generalization of second-order
quantification which permits, so to speak, to quantify upon
an arbitrary sets of ground literals, instead of just (all
ground literals with) a given predicate symbol. We introduce
an operator raise that is only slightly different from
literal projection and can be used to define a
generalization of predicate circumscription in a
straightforward and compact way. We call this variant of
circumscription scope-determined. Some properties of raise
and scope-determined circumscription, also in combination
with literal projection, are then shown. A previously known
characterization of consequences of circumscribed formulas
in terms of literal projection is generalized from
propositional to first-order logic and proven on the basis
of the introduced concepts. The second result developed in
this paper is a characterization stable models in terms of
circumscription. Unlike traditional characterizations, it
does not recur onto syntactic notions like reduct and
fixed-point construction. It essentially renders a recently
proposed ``circumscription-like'' characterization in a
compact way, without involvement of a non-classically
interpreted connective.}
}
@inproceedings{Wernhard:2009:Tableaux,
title = {Tableaux for Projection Computation and Knowledge Compilation},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods:
International Conference, TABLEAUX 2009},
editor = {Martin Giese and Arild Waaler},
pages = {325--340},
year = {2009},
author = {Christoph Wernhard},
publisher = {Springer},
series = {LNAI},
volume = {5607},
url = {http://cs.christophwernhard.com/papers/tableaux-projection.pdf},
doi = {10.1007/978-3-642-02716-1_24},
abstract = {Projection computation is a generalization of second-order
quantifier elimination, which in turn is closely related to
the computation of forgetting and of uniform
interpolants. On the basis of a unified view on projection
computation and knowledge compilation, we develop a
framework for applying tableau methods to these tasks. It
takes refinements from performance oriented systems into
account. Formula simplifications are incorporated at the
level of tableau structure modification, and at the level of
simplifying encountered subformulas that are not yet fully
compiled. In particular, such simplifications can involve
projection computation, where this is possible with low
cost. We represent tableau construction by means of rewrite
rules on formulas, extended with some auxiliary functors,
which is particularly convenient for formula transformation
tasks. As instantiations of the framework, we discuss
approaches to propositional knowledge compilation from the
literature, including adaptions of DPLL, and the hyper
tableau calculus for first-order clauses.}
}
@book{Wernhard:2009:ProjectionElimination,
author = {Christoph Wernhard},
title = {Automated Deduction for Projection Elimination},
number = {324},
series = {Dissertations in Artificial Intelligence},
publisher = {AKA Verlag/IOS Press},
address = {Heidelberg, Amsterdam},
year = {2009},
url = {http://www.iospress.nl/loadtop/load.php?isbn=9781586039837},
abstract = {Projection is a logic operation which allows to express tasks in
knowledge representation. These tasks involve extraction or
removal of knowledge concerning a given sub-vocabulary. It
is a generalization of second-order quantification,
permitting, so to speak, to `quantify' upon an arbitrary set
of ground literals instead of just (all ground literals
with) a given predicate symbol. In \textit{Automated
Deduction for Projection Elimination}, a semantic
characterization of projection for first-order logic is
presented. On this basis, properties underlying applications
and processing methods are derived. The computational
processing of projection, called projection elimination in
analogy to quantifier elimination, can be performed by
adapted theorem proving methods. This is shown for resolvent
generation and, more in depth, tableau construction. An
abstract framework relates projection elimination with
knowledge compilation and shows the adaption of key features
of high performance tableau systems. As a prototypical
instance, an adaption of a modern DPLL method, such as
underlying state-of-the-art SAT solvers, is worked out. It
generalizes various recent knowledge compilation methods and
utilizes the interplay with projection elimination for
efficiency improvements.}
}
@inproceedings{Wernhard:2008:LiteralProjection,
author = {Christoph Wernhard},
title = {Literal Projection for First-Order Logic},
booktitle = {Logics in Artificial Intelligence: 11th
European Conference, JELIA 08},
editor = {Steffen H{\"o}lldobler and Carsten Lutz and Heinrich Wansing},
pages = {389--402},
publisher = {Springer},
series = {LNAI},
volume = {5293},
doi = {10.1007/978-3-540-87803-2_32},
year = {2008},
note = {(Extended version:
\url{http://cs.christophwernhard.com/papers/literal-projection.pdf})},
abstract = {The computation of literal projection generalizes predicate
quantifier elimination by permitting, so to speak,
quantifying upon an arbitrary sets of ground literals,
instead of just (all ground literals with) a given predicate
symbol. Literal projection allows, for example, to express
predicate quantification upon a predicate just in positive
or negative polarity. Occurrences of the predicate in
literals with the complementary polarity are then considered
as unquantified predicate symbols. We present a
formalization of literal projection and related concepts,
such as literal forgetting, for first-order logic with a
Herbrand semantics, which makes these notions easy to
access, since they are expressed there by means of
straightforward relationships between sets of literals. With
this formalization, we show properties of literal projection
which hold for formulas that are free of certain links,
pairs of literals with complementary instances, each in a
different conjunct of a conjunction, both in the scope of a
universal first-order quantifier, or one in a subformula and
the other in its context formula. These properties can
justify the application of methods that construct formulas
without such links to the computation of literal
projection. Some tableau methods and direct methods for
second-order quantifier elimination can be understood in
this way.}
}
@inproceedings{PelzerWernhard:2007:EKrhyper,
author = {Bj{\"o}rn Pelzer and Christoph Wernhard},
title = {System Description: \mbox{E-KRHyper}},
pages = {503--513},
booktitle = {Automated Deduction: \mbox{CADE-21}},
editor = {Frank Pfennig},
publisher = {Springer},
series = {LNAI},
volume = {4603},
url = {http://cs.christophwernhard.com/papers/ekrhyper.pdf},
doi = {10.1007/978-3-540-73595-3_37},
year = {2007},
abstract = {The E-KRHyper system is a model generator and theorem prover for
first-order logic with equality. It implements the new
E-hyper tableau calculus, which integrates a
superposition-based handling of equality into the hyper
tableau calculus. E-KRHyper extends our previous KRHyper
system, which has been used in a number of applications in
the field of knowledge representation. In contrast to most
first order theorem provers, it supports features
important for such applications, for example queries with
predicate extensions as answers, handling of large sets of
uniformly structured input facts, arithmetic evaluation and
stratified negation as failure. It is our goal to extend
the range of application possibilities of KRHyper by adding
equality reasoning.}
}
@techreport{Wernhard:2007:Tableaux,
author = {Christoph Wernhard},
title = {{Tableaux Between Proving, Projection and Compilation}},
institution = {{Universit{\"a}t Koblenz-Landau}},
year = {2007},
number = {Arbeitsberichte aus dem Fachbereich Informatik 18/2007},
address = {Institut f{\"u}r Informatik,
Universit{\"a}tsstr. 1, 56070 Koblenz, Germany},
abstract = {Generalized methods for automated theorem proving can be
used to compute formula transformations such as projection
elimination and knowledge compilation. We present a
framework based on clausal tableaux suited for such
tasks. These tableaux are characterized independently of
particular construction methods, but important features of
empirically successful methods are taken into account,
especially dependency directed backjumping and branch local
operation. As an instance of that framework an adaption of
DPLL is described. We show that knowledge compilation
methods can be essentially improved by weaving projection
elimination partially into the compilation phase.}
}
@inproceedings{Wernhard:2004:SKP,
author = {Christoph Wernhard},
title = {Semantic Knowledge Partitioning},
booktitle = {Logics in Artificial Intelligence:
9th European Conference, JELIA 04},
editor = {Jos{\'e} J{\'u}lio Alferes and Jo{\~a}o Leite Leite},
year = {2004},
pages = {552--564},
publisher = {Springer},
series = {LNAI},
volume = {3229},
url = {http://cs.christophwernhard.com/papers/skp-jelia.ps},
abstract = {Some operations to decompose a knowledge base (considered as a
first order logic formula) in ways so that only its
semantics determines the results are investigated. Intended
uses include the extraction of ``parts'' relevant to an
application, the exploration and utilizing of implicit
possibilities of structuring a knowledge base and the
formulation of query answers in terms of a signature
demanded by an application. A semantic framework based on
Herbrand interpretations is outlined. The notion of ´model
relative to a scopeˇ is introduced. It underlies the
partitioning operations ``projection'' and ``forgetting'' and
also provides a semantic account for certain formula
simplification operations. An algorithmic approach which is
based on resolution and may be regarded as a variation of
the SCAN algorithm is discussed.}
}
@inproceedings{Wernhard:2004:SKPShort,
author = {Christoph Wernhard},
title = {Semantic Knowledge Partitioning (Extended Abstract)},
editor = {Ulrike Sattler},
booktitle = {Contributions to the
Doctoral Programme of the Second International
Joint Conference on Automated Reasoning
(IJCAR 2004)},
series = {CEUR Workshop Proceedings},
volume = {106},
year = {2004},
url = {http://ceur-ws.org/Vol-106/}
}
@inproceedings{BaumgartnerEtAl:2003:KrhyperInside,
author = {Peter Baumgartner and Ulrich Furbach and Margret Gross-Hardt
and Thomas Kleemann and Christoph Wernhard},
title = {{KRH}yper {I}nside -- {M}odel Based Deduction in Applications},
booktitle = {Proceedings of the \mbox{CADE-19} workshop
Challenges and Novel Applications for Automated Reasoning},
year = {2003},
pages = {55-72},
url = {http://cs.christophwernhard.com/papers/novel.ps},
url = {http://www.uclic.ucl.ac.uk/usr/jgow/cnaar.pdf},
abstract = {Three real world applications are depicted which all have a full
first order theorem prover based on the hyper tableau
calculus as their core component. These applications concern
information retrieval in electronic publishing, the
integration of description logics with other knowledge
representation techniques and XML query processing.}
}
@techreport{Wernhard:2003:KRHyper,
author = {Christoph Wernhard},
title = {{System Description: {KRHyper}}},
institution = {{Universit{\"a}t Koblenz-Landau}},
year = {2003},
number = {Fachberichte Informatik 14--2003},
address = {Institut f{\"u}r Informatik,
Universit{\"a}tsstr. 1, 56070 Koblenz, Germany},
note = {Presented at the \mbox{CADE-19} workshop
\textit{Model Computation: Principles, Algorithms, Applications}.},
url = {http://cs.christophwernhard.com/papers/krhsys.ps},
abstract = {KRHyper is a first order logic theorem proving and model
generation system based on the hyper tableau calculus. It is
targeted for use as an embedded system within knowledge
based applications. In contrast to most first order theorem
provers, it supports features important for those
applications, for example queries with predicate extensions
as answers, handling of large sets of uniformly structured
input facts, arithmetic evaluation and stratified negation
as failure.}
}
@unpublished{Wernhard:2002:InfraEngine,
author = {Christoph Wernhard},
title = {{InfraEngine}: {I}nferencing in the {S}emantic {W}eb by Planning},
year = {2002},
note = {System description (edited 2007). (A prototype implementation can be
downloaded from \url{http://www.infraengine.com/})},
url = {http://www.infraengine.com/papers/infra.pdf},
abstract = {The idea of InfraEngine is to help establishing a Semantic Web
infrastructure by a specially adapted AI planning
engine. Inputs are distributed Web documents in Semantic Web
formats proposed by the World Wide Web Consortium. Outputs
are also delivered in such formats. The user interface
allows to browse Semantic Web data and to control the
planning services from any Web browser. Also other programs
can make use of these services. A small and understandable,
but general, mechanism that can be used for different kinds
of applications should be provided.}
}
@unpublished{Wernhard:2001:SemWebProofs,
author = {Christoph Wernhard},
title = {Representing Proofs in the {S}emantic {W}eb},
year = {2001},
note = {Working paper for Persist AG, Teltow, Germany},
url = {http://cs.christophwernhard.com/papers/papers/persist/swproofs.pdf},
abstract = {First steps towards an RDF format for exchanging proofs in the
Semantic Web.}
}
@unpublished{Wernhard:2000:SemWebApplications,
author = {Christoph Wernhard},
title = {Two Short Term Applications of the {S}emantic {W}eb},
year = {2001},
note = {Working paper for Persist AG, Teltow, Germany},
url = {http://cs.christophwernhard.com/papers/persist/applic.pdf},
abstract = {We outline two application scenarios which might be in the realm
of short term applications of the Semantic Web: a software
packaging system and the organization of a business
trip. Both of them can be solved with today's technology to
some degree, so they do not show the novel potential of the
Semantic Web in full. However considering Semantic Web
solutions for them is useful to get a picture of the
characteristics of the Semantic Web and become aware of some
concrete technical issues.}
}
@unpublished{Wernhard:2000:PlanningWeb,
author = {Christoph Wernhard},
title = {The {P}lanning {W}eb in Action},
year = {2000},
note = {Working paper for Persist AG, Teltow, Germany},
url = {http://cs.christophwernhard.com/papers/persist/outline.pdf},
abstract = {We propose resource oriented inference as one way of bringing the
Semantic Web into action. It provides a framework for
expressing and processing a variety of tasks from areas such
as planning, scheduling, manufacturing resource planning,
product data management, configuration management, workflow
management and simulation. Resource oriented inference as a
part of the Semantic Web should allow such tasks to be
performed within the scope of the World Wide Web. A
prototypical application is be the purchase of a complex
product with the help of the Web. The product consists of
multiple parts, some of them complex products by
themselves. Several services are required to compose the
product. Subparts and services can be provided by different
companies all over the world. Delivery time and cost of the
product should be optimized.}
}
@unpublished{Wernhard:2000:SemanticWebModelin,
author = {Christoph Wernhard},
title = {Towards a {S}emantic {W}eb Modeling Language},
year = {2000},
note = {Working paper for Persist AG, Teltow, Germany. Presented
at \textit{KnowTech 2000}, Leipzig},
url = {http://cs.christophwernhard.com/papers/persist/swmod.pdf},
abstract = {Outline of a small Web embedded language for specifying types and
reasoning about them. Its main features are: (1.) From
primitive types, that require from their instances just that
they implement a single method, complex types can be
constructed by a few operators, such as as a type
intersection. This composition of type definitions maps to
the composition of fragments of type definitions in
different Web documents. (2.) Types are compared by
structural equivalence and not based on their names. This
facilitates combination of independently developed models
and implicit association of types with given instances. (3.)
The hyperlinking of expressions of the modeling language can
be understood in terms of defining equations of a rewriting
system. The left side of such a rewrite rule is an URI, the
right side an expression. Hyperlink dereferencing
corresponds to a rewrite step with such a rule.}
}
@unpublished{Wernhard:1999:LBCP,
author = {Christoph Wernhard},
title = {Experiments with a Linear Backward Chaining Planner},
url = {http://cs.christophwernhard.com/papers/exp.ps},
year = {1999},
note = {(Edited May 2003)},
abstract = {The performance of an implementation of the linear backward
chaining planning algorithm is compared to other planning
systems by means of the problem set of the first ai planning
systems competition (AIPS-98).}
}
@inproceedings{DahnEtAl:1998:MathlibMathematica,
author = {Ingo Dahn and Andreas Haida and Thomas Honigmann and
Christoph Wernhard},
title = {Using {M}athematica and Automated Theorem Provers to Access a
Mathematical Library},
booktitle = {Proceedings of the \mbox{CADE-15} workshop on
Integration of Deductive Systems},
pages = {36--43},
note = {(Revised and extended version:
\url{http://cs.christophwernhard.com/papers/integ.ps})},
url = {http://i12www.ira.uka.de/Workshop/notes.ps.gz},
year = {1998},
abstract = {We describe a concept for the cooperation of a computer
algebra system, several automated theorem provers and a
mathematical library. The purpose of this cooperation is to
enable intelligent retrieval of theorems and definitions
from the remote mathematical library. Automated theorem
provers compete on remote machines to verify conjectures
provided by the user in a local copy of Mathematica. They
make use of a remote knowledge base which contains parts of
the Mizar Mathematical Library.}
}
@inproceedings{DahnWernhard:1997:Mathlib,
author = {Ingo Dahn and Christoph Wernhard},
title = {First Order Proof Problems Extracted from an Article in the
{Mizar} Mathematical Library},
booktitle = {International
Workshop on First-Order Theorem Proving, FTP'97},
year = {1997},
series = {RISC-Linz Report Series No.\ 97--50},
pages = {58--62},
publisher = {Johannes Kepler Universit{\"a}t, Linz, Austria},
url = {http://cs.christophwernhard.com/papers/ftp97.ps},
abstract = {Over the years, interactive theorem provers have built a large
body of verified computer mathematics. The ILF Mathematical
Library aims to make this knowledge available to other
systems. One of the reasons for such a project is
economy. Verification of software and hardware frequently
requires the proof of purely mathematical theorems. It is
obviously inefficient, to use the time of experts in the
design of software or hardware systems to prove such
theorems. Another reason for presenting a collection of
mathematical theorems in a unified framework is safety. It
should facilitate the verification of theorems in the
library of one system by other systems. A third reason is
dynamics of research. New interactive theorem provers should
obtain the possibility to show their usability for
real-world problems without having to reprove elementary
mathematical facts. Last but not least, it is hoped that
reproving theorems in a uniform mathematical library will be
considered as a challenge to the development of automated
theorem provers.}
}
@mastersthesis{Wernhard:92:CLOSDB,
author = {Christoph Wernhard},
title = {Entwurf und {I}mplementierung einer
{D}atenbank\-schnitt\-stelle
f{\"u}r das {C}ommon {L}isp {O}bject {S}ystem},
school = {Freie Universit{\"a}t Berlin},
address = {Berlin, Germany},
type = {Magisterarbeit},
year = {1992},
note = {(The system documentation is available from
\url{http://cs.christophwernhard.com/cdb/}.)}
}
@inproceedings{SchweppeEtAl:90:DBCLOS,
author = {Heinz Schweppe and Christoph Wernhard and Jutta Estenfeld},
title = {{DB-CLOS}: {E}ine {D}atenbankschnittstelle f{\"u}r das
{C}ommon {L}isp {O}bject {S}ystem},
booktitle = {K{\"u}nstliche Intelligenz in der Praxis},
year = {1990},
publisher = {Siemens AG},
editor = {W. Remmele}
}