System f2lp – computing answer sets of first-order formulas. We present an implementation of the general language of stable models proposed by Ferraris, Lee and Lifschitz. Under certain conditions, system f2lp turns a first-order theory under the stable model semantics into an answer set program, so that existing answer set solvers can be used for computing the general language. Quantifiers are first eliminated and then the resulting quantifier-free formulas are turned into rules. Based on the relationship between stable models and circumscription, f2lp can also serve as a reasoning engine for general circumscriptive theories. We illustrate how to use f2lp to compute the circumscriptive event calculus.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Bartholomew, Michael; Lee, Joohyung: System ASPMT2SMT: computing ASPMT theories by SMT solvers (2014)
- Babb, Joseph; Lee, Joohyung: Cplus 2ASP: computing action language $\cal C$+ in answer set programming (2013)
- Ferraris, Paolo; Lee, Joohyung; Lierler, Yuliya; Lifschitz, Vladimir; Yang, Fangkai: Representing first-order causal theories by logic programs (2012)
- Pearce, D.; Valverde, A.: Synonymous theories and knowledge representations in answer set programming (2012)
- Cabalar, Pedro; Santos, Paulo E.: Formalising the Fisherman’s Folly puzzle (2011)
- Casolary, Michael; Lee, Joohyung: Representing the language of the causal calculator in answer set programming (2011)