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.
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