EqWB

The Equilibrium Logic Workbench¹

1. Tools for Here-and-There and Equilibrium Logic

• qht.pl
  
  This program takes as an input an arbitrary first order theory from Quantified Here-and-There and uses the translation into classical logic presented in [LPV07] to generate a file to be processed by the theorem prover Prover9. Among other uses, this tool can be applied to check strong equivalence of logic programs with variables: we just write their equivalence, call qht.pl and then wait for Prover9 answer for the result.
  
  
• minlp.pl
  
  This is a Prolog program that accepts as input an arbitrary propositional theory and generates one (or more) equivalent disjuntive ground logic program (possibly with negation in the head) that are syntactically minimal. As shown in [CF07], under equilibrium logic, any arbitrary theory is strongly equivalent to a logic program. The tool implements the method presented in [CPV07] to obtain a minimal logic program from the set of countermodels of an arbitrary theory, using a similar technique to Quine-McCluskey's algorithm for minimising boolean functions. The tool can be used to simplify a logic program (removing redundant literals and rules) or to obtain the simplest logic program representation of an arbitrary propositional expressions. For further help, call predicate help(minlp). This program has been used to generate the list of 162 possible (minimal) logic programs for 2 variables.
  
  
• rptlp.pl, polytrans.pl
  
  These two programs are similar to minlp.pl in the sense that they allow transforming arbitrary propositional theories into ground logic programs. The main difference is that they do not guarantee syntactic minimality. However, they are usually faster than minlp, as they do not generate the set of countermodels. Both programs implement the two transformations presented in [CPV05]. The first transformation rptlp.pl is exponential, but maintains the original propositional alphabet, whereas the second one polytrans.pl is polynomial but at the cost of introducing auxiliary atoms. To invoke rptlp.pl just call predicate write_transform(F) with F a propositional formula: the resulting program is printed in the screen. If you previously call assert(show_steps), all the intermediate transformation steps are shown too. For polytrans.pl call predicate lp(F,Rs), with F a propositional formula and Rs the set of resulting rules.
  
  
• htcheck.pl
  
  This program computes the Equilibrium and Here-and-There models of an arbitrary theory. Models are organised following the models minimisation criterion of Equilibrium Logic. It also allows checking strong equivalence of two theories or programs by blind-force comparison of their sets of Here-and-There models.
  
  
• tabeql
  
  This program is written in Caml language and implements semantic tableaux procedures for:
  
• computing the equilibrium models of an arbitrary theory [PGV00]
  
• checking the strong equivalence between two arbitrary theories
• checking the uniform equivalence (i.e., the same behaviour wrt addition of atoms) between two arbitrary theories

2. Tools for Partial Equilibrium Logic

• wfht.pl
  
  This program allows computing several semantics related to Well-Founded Semantics [GRS91] and Partial Equilibrium Logic [COPV07] . The program allows computing the Partial Equilibrium Models [COPV07], the Back-and-Forth semantics [] and the Infinite Valued Semantics of []. Once loaded in the prolog interpreter, type help for more information.
  

3. High level languages: Action Theories, Computational Societies, etc

• Functional Action Language
  

Acknowledgements

REFERENCES