Abstract
A prototype system is described whose core functionality is, based on propositional logic, the elimination of second-order operators, such as Boolean quantifiers and operators for projection, forgetting and circumscription. This approach allows to express many representational and computational tasks in knowledge representation – for example computation of abductive explanations and models with respect to logic programming semantics – in a uniform operational system, backed by a uniform classical semantic framework.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
http://cs.christophwernhard.com/toyelim/, under GNU Public License.
References
Gabbay, D.M., Schmidt, R.A., Szałas, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications, London (2008)
Huang, J., Darwiche, A.: DPLL with a trace: from SAT to knowledge compilation. In: IJCAI-05, pp. 156–162. Morgan Kaufmann (2005)
Kakas, A.C., Kowalski, R.A., Toni, F.: Abductive logic programming. J. Logic Comput. 2(6), 719–770 (1993)
Lang, J., Liberatore, P., Marquis, P.: Propositional independence - formula-variable independence and forgetting. J. Artif. Intell. Res. 18, 391–443 (2003)
Lifschitz, V.: Circumscription. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 298–352. Oxford University Press, Oxford (1994)
Lifschitz, V.: Twelve definitions of a stable model. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 37–51. Springer, Heidelberg (2008)
Lin, F.: A study of nonmonotonic reasoning. Ph.D. thesis, Stanford University (1991)
Lin, F.: On strongest necessary and weakest sufficient conditions. Artif. Intell. 128, 143–159 (2001)
Manthey, N.: Coprocessor 2.0 – a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436–441. Springer, Heidelberg (2012)
Murray, N.V., Rosenthal, E.: Tableaux, path dissolution and decomposable negation normal form for knowledge compilation. In: Mayer, M.C., Pirri, F. (eds.) TABLEAUX 2003. LNCS (LNAI), vol. 2796, pp. 165–180. Springer, Heidelberg (2003)
Wernhard, C.: Literal projection for first-order logic. In: Hölldobler, S., Lutz, C., Wansing, H. (eds.) JELIA 2008. LNCS (LNAI), vol. 5293, pp. 389–402. Springer, Heidelberg (2008)
Wernhard, C.: Tableaux for projection computation and knowledge compilation. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 325–340. Springer, Heidelberg (2009)
Wernhard, C.: Circumscription and projection as primitives of logic programming. In: Technical Communications of the ICLP 2010. LIPIcs, vol. 7, pp. 202–211 (2010)
Wernhard, C.: Forward human reasoning modeled by logic programming modeled by classical logic with circumscription and projection. Technical Report Knowledge Representation and Reasoning 11-07, Technische Universität Dresden (2011)
Wernhard, C.: Projection and scope-determined circumscription. J. Symb. Comput. 47, 1089–1108 (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wernhard, C. (2013). Computing with Logic as Operator Elimination: The ToyElim System. In: Tompits, H., et al. Applications of Declarative Programming and Knowledge Management. INAP WLP 2011 2011. Lecture Notes in Computer Science(), vol 7773. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41524-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-41524-1_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41523-4
Online ISBN: 978-3-642-41524-1
eBook Packages: Computer ScienceComputer Science (R0)