# The ToyElim System

An experimental prototype system for the computational processing of logic
formulas. It is 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.

## Caveats

This system is currently intended just as a vehicle for
experiments of various kinds. The code is of miscellaneous quality and
robustness.
## Downloads

- The
*ToyElim* system (runs
with SWI-Prolog)

The following is also included in the system archive:

System Version |
Changelog |
Installation |
User Manual |
Configuration
Options

- Examples

Simple
Examples

An Example
Factbase with "Realworld" Facts (about Dresden) |
Some
"Realworld" Examples

Simple Examples with
Semantics for Logic Programming

Examples with
Abduction for the Stable and Partial Stable
Model Semantics

Examples for
Second-Order Quantifier Elimination Based on
First-Order Logic

Toy Examples for
Computing Definientia in Formula Classes
- System Description:
*Computing with Logic as Operator
Elimination: The ToyElim System.*
Also published as:
Christoph
Wernhard, *Computing with Logic as Operator Elimination: The ToyElim
System.* In Hans Tompits, Salvador Abreu, Johannes Oetsch,
Jörg Pührer, Dietmar Seipel, Masanobu Umeda, and Armin Wolf,
editors, Applications of Declarative Programming and Knowledge Management,
19th International Conference (INAP 2011) and 25th Workshop on Logic
Programming(WLP 2011), Revised Selected Papers, volume 7773 of
LNCS (LNAI), pages 289-296. Springer, 2013

- Old versions of the
*ToyElim* system