Software

• ToyElim
  Experimental prototype of an “elimination based” system for the computational processing of logics (under development)
  
  • 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 external solvers.
• Story
  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 Firefox 3.
• KRHyper
  First order logic theorem proving and model generation system (2003-2005)
  • 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 Prolog.
  • 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 applications.
• InfraEngine
  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 representations.

  Runs as a Web server, providing a Web user interface. Implemented in SWI Prolog.

• Liner
  Planning system (1999, revised 2002 and 2007)
  • Prototype implementation of the linear backward chaining (LBC) planning algorithm by Bertram Fronhöfer, a variant of the linear connection method by Wolfgang Bibel.
  • Runs in the SWI-Prolog environment. Outputs are represented by Prolog terms. Plans can also be displayed as images of graphs.
  • Operates by compiling planning tasks to Prolog code, similar to the Prolog Technology Theorem Prover (PTTP) by Mark Stickel.
  • Has been in combined in the InfraEngine system with an RDF interface.
• CM
  First order theorem prover (1992, revised 1997)

  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.

• CLOS-DB
  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.