Prolog-based environment for first-order-based proving, interpolating and
eliminating, successor to ToyElim (2015-...)
An experimental system to investigate
possibilities of knowledge-based support for scholarly editing and text
Experimental prototype of an “elimination
based” system for the computational processing of logics
- Centered around a single processing function which
takes a formula of propositional logic extended with
operators for projection and circumscription as input, and
outputs an equivalent formula without these operators.
- Tasks like elimination of Boolean quantifiers,
computation of uniform interpolants, certain forms of
abduction, SAT and QBF solving, and processing of formulas
according to various semantics of logic programming can be
expressed and integrated in this framework.
- The objective of the system is to explore experimentally
the approach to the computational processing of logics by
operator elimination. The current implementation is
basically a toy system which suffices for small
applications. It however transparently passes identified
SAT, QBF and variable elimination subproblems to efficient
System to support scholarly editing, in
particular the representation of archives
with correspondences (2012-2013)
Prototype of a simple Web browsing
history browser (2007)
- Anything is automatically derived from browsing logs. During
browsing, there is no special user activity – like
bookmarking – required.
- Orientation by means of the terms looked up via Google searches.
- Any information about the browsing history fully
remains private. No social networking.
- Runs as a Web server, providing a Web user interface.
- Implemented in SWI Prolog,
utilizing the new Places database interface to browsing
history information of
First-order logic theorem proving and model generation system
- Based on the
hyper tableau calculus by Peter Baumgartner, Uli Furbach
and Ilkka Niemelä.
- Reimplementation and continuation of the original
KRHyper system by Peter Baumgartner, which was written in
- Has been extended with superposition based equality
handling by Björn Pelzer in 2007.
- Implemented in OCaml.
- Supports features for knowledge based applications
that can not usually be found in first-order provers. For
example queries with predicate extensions as answers, handling
of large sets of uniformly structured input facts, arithmetic
evaluation, and stratified negation as failure
- Robust and used in several
Combination of an RDF Schema browser with a planning engine
(2002, revised 2007)
A working prototype of a Semantic Web engine that combines
- RDF Schema browsing, where
Semantic Web processing is integrated with
“normal” browsing and
Schema inferences corresponding to the model
theoretic semantics of RDF
are transparently performed
- with a planning engine, where
in- and outputs of planning tasks have RDF
Runs as a Web server, providing a Web user interface. Implemented
in SWI Prolog.
Planning system (1999, revised 2002 and 2007)
First-order theorem prover (1992, revised 1997 and 2015)
Model elimination prover, heavily influenced by PTTP and Setheo
(without knowing about Mark Stickel's implementation of PTTP in
Prolog). Written in Prolog; operates by compiling a proof task
into a Prolog program. The 1997 version was used along with other
provers in experiments with translations
of parts the Mizar Mathematical Library.
Database interface for the Common Lisp Object System (CLOS) (1992)
Allows to specify mappings between classes and relations. Has been
prototypically implemented with the CLOS Metaobject Protocol
AMOP. The specification along
with an example is online.