Navegar

Colección

Datos Estadísticas

Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

We investigate labeled resolution calculi for hybrid logics with inference rules restricted via selection functions and orders. We start by providing a sound and refutationally complete calculus for the hybrid logic H(at ↓,A), even under restrictions by selection functions and orders. Then, by imposing further restrictions in the original calculus, we develop a sound, complete and terminating calculus for the H(at) sublanguage. The proof scheme we use to show refutational completeness of these calculi is an adaptation of a standard completeness proof for saturation-based calculi for first-order logic that guarantees completeness even under redundancy elimination. In fact, one of the contributions of this article is to show that the general framework of saturation-based proving for first-order logic with equality can be naturally adapted to saturation-based calculi for other languages, in particular modal and hybrid logics. © 2010 Springer Science+Business Media B.V.

Registro:

Documento: Artículo
Título:Resolution with order and selection for hybrid logics
Autor:Areces, C.; Gorín, D.
Filiación:Talaris Group, INRIA Nancy Grand Est, Nancy, France
Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina
Palabras clave:Modal logic; Order and selection function constraints; Resolution calculus; Soundness and completeness; Termination; Modal logic; Order and selection function constraints; Resolution calculus; Soundness and completeness; Termination; Biomineralization; Formal logic; Pathology; Calculations
Año:2011
Volumen:46
Número:1
Página de inicio:1
Página de fin:42
DOI: http://dx.doi.org/10.1007/s10817-010-9167-0
Título revista:Journal of Automated Reasoning
Título revista abreviado:J Autom Reasoning
ISSN:01687433
CODEN:JAREE
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_01687433_v46_n1_p1_Areces

Referencias:

  • Abadi, M., Manna, Z., Modal theorem proving (1986) Proceedings of the 8th International Conference on Automated Deduction, pp. 172-189
  • Abadi, M., Manna, Z., A timely resolution (1986) Proceedings of the 1st IEEE Symposium on Logic in Computer Science, pp. 176-186
  • Achmidt, R., A new methodology for developing deduction methods (2009) Ann. Math. Artif. Intell., 55 (12), pp. 155-187. , 2549973
  • Areces, C., (2000) Logic Engineering. The Case of Description and Hybrid Logics, , Ph.D. thesis, Institute for Logic, Language and Computation, University of Amsterdam
  • Areces, C., Blackburn, P., Marx, M., A road-map on complexity for hybrid logics (1999) Proceedings of the 8th Annual Conference of the EACSL, pp. 307-321
  • Areces, C., Blackburn, P., Marx, M., The computational complexity of hybrid temporal logics (2000) Log. J. IGPL, 8 (5), pp. 653-679. , 0959.03011 10.1093/jigpal/8.5.653 1783899
  • Areces, C., De Rijke, M., De Nivelle, H., Resolution in modal, description and hybrid logic (2001) Journal of Logic and Computation, 11 (5), pp. 717-736. , DOI 10.1093/logcom/11.5.717
  • Areces, C., Gennari, R., Heguiabehere, J., De Rijke, M., Tree-based heuristics in modal theorem proving (2000) Proceedings of ECAI 2000, pp. 199-203. , Horn, W. (ed.)
  • Areces, C., Gorín, D., Ordered resolution with selection for H at (2005) Proceedings of LPAR 2004. LNCS, 3452, pp. 125-141. , F. Baader A. Voronkov (eds). Springer New York
  • Areces, C., Ten Cate, B., Hybrid logics (2006) Handbook of Modal Logics, pp. 821-868. , P. Blackburn F. Wolter J. van Benthem (eds). Elsevier Amsterdam
  • Auffray, Y., Enjalbert, P., Hebrard, J., Strategies for modal resolution: Results and problems (1990) J. Autom. Reason., 6 (1), pp. 1-38. , 0709.03008 10.1007/BF00302639 1060445
  • Baader, F., Nipkow, T., (1998) Term Rewriting and All That, , Cambridge University Press Cambridge
  • Bachmair, L., Ganzinger, H., Equational reasoning in saturation-based theorem proving (1998) Automated Deduction-a Basis for Applications, Vol. I, pp. 353-397. , Kluwer Boston
  • Bachmair, L., Ganzinger, H., Resolution theorem proving (2001) Handbook of Automated Reasoning, Vol. 1, Chap. 2, pp. 19-99. , J. Robinson A. Voronkov (eds). Elsevier Amsterdam. 10.1016/B978- 044450813-3/50004-7
  • Bieber, P., MOLOG: A modal PROLOG (1988) Proceedings of the 9th International Conference on Automated Deduction, pp. 762-763
  • Blackburn, P., Representation, reasoning, and relational structures: A hybrid logic manifesto (2000) Log. J. IGPL, 8 (3), pp. 339-365. , 0956.03025 10.1093/jigpal/8.3.339 1768949
  • Blackburn, P., De Rijke, M., Venema, Y., (2002) Modal Logic, , Cambridge University Press Cambridge
  • (2006) Handbook of Modal Logics, , P. Blackburn F. Wolter J. van Benthem (eds). Elsevier Amsterdam
  • Cialdea, M., Fariñas Del Cerro, L., A modal Herbrand's property (1986) Z. Math. Log. Grundl. Math., 32, pp. 523-530. , 0589.03004 10.1002/malq.19860323106
  • Clarke, E., Grumberg, O., Peled, D., (2000) Model Checking, , MIT Cambridge
  • De Nivelle, H., De Rijke, M., Deciding the guarded fragments by resolution (2003) Journal of Symbolic Computation, 35 (1), pp. 21-58. , DOI 10.1016/S0747-7171(02)00092-5
  • De Nivelle, H., Schmidt, R., Hustadt, U., Resolution-based methods for modal logics (2000) Log. J. IGPL, 8 (3), pp. 265-292. , 0947.03014 10.1093/jigpal/8.3.265 1768946
  • Enjalbert, P., Fariñas Del Cerro, L., Modal resolution in clausal form (1989) Theor. Comp. Sci., 65 (1), pp. 1-33. , 0669.03009 10.1016/0304-3975(89)90137-0
  • Fariñas Del Cerro, L., A simple deduction method for modal logic (1982) Inf. Process. Lett., 14 (2), pp. 47-51
  • Fariñas Del Cerro, L., Resolution modal logic (1985) Logics and Models of Concurrent Systems, pp. 27-55. , K. Apt (eds). Springer Berlin
  • Fariñas Del Cerro, L., MOLOG: A system that extends PROLOG with modal logic (1986) New Gener. Comput., 4 (1), pp. 35-50. , 0598.68063 10.1007/BF03037381
  • Fitting, M., Destructive modal resolution (1990) J. Log. Comput., 1 (1), pp. 83-97. , 0724.03011 10.1093/logcom/1.1.83 1165239
  • Ganzinger, H., De Nivelle, H., A superposition decision procedure for the guarded fragment with equality (1999) LICS '99: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p. 295. , IEEE Computer Society Los Alamitos
  • Giese, M., Ahrendt, W., Hilbert's ε-terms in automated theorem proving (1999) Automated Reasoning with Analytic Tableaux and Related Methods, Intl. Conf. (TABLEAUX'99). LNAI, 1617, pp. 171-185. , N. Murray (eds). Springer Berlin. 10.1007/3-540-48754-9-17
  • Grädel, E., On the restraining power of guards (1999) J. Symb. Log., 64, pp. 1719-1742. , 0958.03027 10.2307/2586808
  • Grädel, E., Why are modal logics so robustly decidable? (2001) Current Trends in Theoretical Computer Science: Entering the 21st Centuary, pp. 393-408. , World Scientific Singapore
  • Herbrand, J., (1930) Recherches sur la Théorie de la Démonstrations, , Ph.D. thesis, Sorbone Reprinted In: Goldfarb, W. (ed.) Logical Writings. Reidel, Dordrecht
  • Hilbert, D., Bernays, P., (1939) Grundlagen der Mathematik, Vol. 2, , Springer Berlin
  • Hustadt, U., Schmidt, R.A., Using resolution for testing modal satisfiability and building models (2002) Journal of Automated Reasoning, 28 (2), pp. 205-232. , DOI 10.1023/A:1015067300005
  • Kazakov, Y., (2006) Saturation-based Decision Procedures for Extensions of the Guarded Fragment, , Ph.D. thesis, Universität des Saarlandes
  • Kazakov, Y., Motik, B., A resolution-based decision procedure for SHOIQ (2008) J. Autom. Reason., 40 (23), pp. 89-116. , 1137.68056 10.1007/s10817-007-9090-1 2418642
  • Knuth, D., Bendix, P., Simple word problems in universal algebras (1970) Computational Algebra, pp. 263-297. , J. Leech (eds). Pergamon Oxford
  • Leisenring, A., (1969) Mathematical Logic and Hilbert's ε-symbol, , MacDonald London
  • Lindström, S., Segerberg, K., Modal logic and philosophy (2006) Handbook of Modal Logics, pp. 1149-1214. , P. Blackburn F. Wolter J. van Benthem (eds). Elsevier Amsterdam
  • Mints, G., Resolution calculi for modal logics (1989) Am. Math. Soc. Transl., 143, pp. 1-14
  • Mints, G., Gentzen-type systems and resolution rules, part 1: Propositional logic (1990) Proceedings of COLOG-88, Tallin. Lecture Notes in Computer Science, 417, pp. 198-231. , Springer Berlin
  • Nalon, C., Dixon, C., Clausal resolution for normal modal logics (2007) Journal of Algorithms, 62 (3-4), pp. 117-134. , DOI 10.1016/j.jalgor.2007.04.001, PII S0196677407000302
  • Nieuwenhuis, R., Rubio, A., Paramodulation-based theorem proving (2001) Handbook of Automated Reasoning, Vol. 1, Chap. 7, pp. 371-443. , A. Robinson A. Voronkov (eds). Elsevier Amsterdam. 10.1016/B978- 044450813-3/50009-6
  • Ohlbach, H., (1988) A Resolution Calculus for Modal Logics, , Ph.D. thesis, Universität Kaiserslautern
  • Riazanov, A., Voronkov, A., Vampire 1.1 (System Description) (2001) JCAR '01: Proceedings of the First International Joint Conference on Automated Reasoning, (2083), pp. 376-380. , Automated Reasoning
  • (2001) Handbook of Automated Reasoning, , A. Robinson A. Voronkov (eds). Elsevier Amsterdam 0964.00020
  • Robinson, J., A machine-oriented logic based on the resolution principle (1965) J. ACM, 12 (1), pp. 23-41. , 0139.12303 10.1145/321250.321253
  • Schmidt, R., Resolution is a decision procedure for many propositional modal logics (1998) Advances in Modal Logic, Vol. 1, pp. 189-208. , CSLI Stanford
  • Schmidt, R., Decidability by resolution for propositional modal logics (1999) J. Autom. Reason., 22 (4), pp. 379-396. , 0924.68178 10.1023/A:1006043519663
  • Schmidt, R.A., Hustadt, U., Mechanised Reasoning and Model Generation for Extended Modal Logics (2003) Lecture Notes in Computer Science, (2929), pp. 38-67. , Theory and Applications of Relational Structures as Knowledge Instruments COST Action 274, TARSKI Revised Papers
  • Vardi, M., Why is modal logic so robustly decidable? (1997) DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 31, pp. 149-184. , 31 AMS Providence
  • Voronkov, A., Algorithms, Datastructures, and Other Issues in Efficient Automated Deduction (2001) Lecture Notes in Computer Science, (2083), pp. 13-28. , Automated Reasoning
  • Weidenbach, C., System description: SPASS version 1.0.0 (1999) CADE-16: Proceedings of the 16th International Conference on Automated Deduction, pp. 378-382. , Springer Berlin. 10.1007/3-540-48660-7-34

Citas:

---------- APA ----------
Areces, C. & Gorín, D. (2011) . Resolution with order and selection for hybrid logics. Journal of Automated Reasoning, 46(1), 1-42.
http://dx.doi.org/10.1007/s10817-010-9167-0
---------- CHICAGO ----------
Areces, C., Gorín, D. "Resolution with order and selection for hybrid logics" . Journal of Automated Reasoning 46, no. 1 (2011) : 1-42.
http://dx.doi.org/10.1007/s10817-010-9167-0
---------- MLA ----------
Areces, C., Gorín, D. "Resolution with order and selection for hybrid logics" . Journal of Automated Reasoning, vol. 46, no. 1, 2011, pp. 1-42.
http://dx.doi.org/10.1007/s10817-010-9167-0
---------- VANCOUVER ----------
Areces, C., Gorín, D. Resolution with order and selection for hybrid logics. J Autom Reasoning. 2011;46(1):1-42.
http://dx.doi.org/10.1007/s10817-010-9167-0