Abstract
This paper analyses the idea of strong equivalence for transition systems represented as logic programs under the Answer Set Programming (ASP) paradigm. To check strong equivalence, we use a linear temporal extension of Equilibrium Logic (a logical characterisation of ASP) and its monotonic basis, the intermediate logic of Here-and-There (HT). Trivially, equivalence in this temporal extension of HT provides a sufficient condition for temporal strong equivalence and, as we show in the paper, it can be transformed into a provability test into the standard Linear Temporal Logic (LTL), something that can be automatically checked using any of the LTL available provers. The paper shows an example of the potential utility of this method by detecting some redundant rules in a simple actions reasoning scenario.
This research is partially supported by Spanish Ministry MEC, research project TIN-15455-C03-02.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Marek, V., Truszczyński, M.: Stable models and an alternative logic programming paradigm. In: The Logic Programming Paradigm: a 25-Year Perspective, pp. 169–181. Springer, Heidelberg (1999)
Niemelä, I.: Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 241–273 (1999)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K.A. (eds.) Logic Programming: Proc.of the Fifth International Conference and Symposium, vol. 2, pp. 1070–1080. MIT Press, Cambridge (1988)
Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving, pp. 285–316. Elsevier, Amsterdam (2003)
Gelfond, M.: Answer Sets. In: Handbook of Knowledge Representation, pp. 285–316. Elsevier, Amsterdam (2007)
WASP: ASP solvers web page (last update, 2005), http://dit.unitn.it/~wasp/Solvers/index.html
Pearce, D.: A new logical characterisation of stable models and answer sets. In: Dix, J., Przymusinski, T.C., Moniz Pereira, L. (eds.) NMELP 1996. LNCS, vol. 1216. Springer, Heidelberg (1997)
Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. Computational Logic 2(4), 526–541 (2001)
Pearce, D., Valverde, A.: Towards a first order equilibrium logic for nonmonotonic reasoning. In: Alferes, J.J., Leite, J.A. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 147–160. Springer, Heidelberg (2004)
Ferraris, P., Lee, J., Lifschitz, V.: A new perspective on stable models. In: Proc. of the International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 372–379 (2004)
McCarthy, J., Hayes, P.: Some philosophical problems from the standpoint of artificial intelligence. Machine Intelligence Journal 4, 463–512 (1969)
Giunchiglia, E., Lee, J., Lifschitz, V., McCain, N., Turner, H.: Nonmonotonic causal theories. Artificial Intelligence Journal 153, 49–104 (2004)
Ferraris, P.: Causal theories as logic programs. In: Proc. of the 20th Workshop on Logic Programming (WLP 2006) (2006)
Gelfond, M., Lifschitz, V.: Action languages. Linköping Electronic Articles in Computer and Information Science 3(16) (1998)
Eiter, T., Faber, W., Traxler, P.: Testing strong equivalence of datalog programs - implementation and examples. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 437–441. Springer, Heidelberg (2005)
Cabalar, P.: QHT - a prover for quantified here and there (2008), http://www.dc.fi.udc.es/~cabalar/eqwb.html
Lifschitz, V., Pearce, D., Valverde, A.: A characterization of strong equivalence for logic programs with variables. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol. 4483. Springer, Heidelberg (2007)
Heyting, A.: Die formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preussischen Akademie der Wissenschaften. Physikalisch-mathematische Klasse, 42–56 (1930)
Cabalar, P., Vega, G.P.: Temporal equilibrium logic: a first approach. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol. 4739, pp. 241–248. Springer, Heidelberg (2007)
Kamp, J.A.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California at Los Angeles (1968)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)
Pearce, D., Tompits, H., Woltran, S.: Encodings of equilibrium logic and logic programs with nested expressions. In: Bradzil, P., Jorge, A. (eds.) EPIA 2001. LNCS (LNAI), vol. 2258, pp. 306–320. Springer, Heidelberg (2001)
Lin, F.: Reducing strong equivalence of logic programs to entailment in classical propositional logic. In: Bradzil, P., Jorge, A. (eds.) Proc. of the 8th Intl. Conf. on Principles and Knowledge Representation and Reasoning (KR 2002), pp. 170–176. Morgan Kaufmann, San Francisco (2002)
Heuerding, A., Jäger, G., Schwendimann, S., Seyfried, M.: A logics workbench. AI Communications 9(2), 53–58 (1996)
Thielscher, M.: Ramification and causality. Artificial Intelligence Journal 89(1–2), 317–364 (1997)
Valverde, A.: tabeql: A tableau based suite for equilibrium logic. In: Alferes, J.J., Leite, J.A. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 734–737. Springer, Heidelberg (2004)
Chen, Y., Lin, F., Li, L.: SELP - a system for studying strong equivalence between logic programs. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 442–446. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aguado, F., Cabalar, P., Pérez, G., Vidal, C. (2008). Strongly Equivalent Temporal Logic Programs. In: Hölldobler, S., Lutz, C., Wansing, H. (eds) Logics in Artificial Intelligence. JELIA 2008. Lecture Notes in Computer Science(), vol 5293. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87803-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-87803-2_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87802-5
Online ISBN: 978-3-540-87803-2
eBook Packages: Computer ScienceComputer Science (R0)