Mostrar el registro sencillo del ítem

dc.contributor.authorRocha, Camilo
dc.contributor.authorMeseguer, José
dc.date.accessioned2021-12-07T17:19:23Z
dc.date.available2021-12-07T17:19:23Z
dc.date.issued2008
dc.identifier.isbn9783540789130
dc.identifier.isbn9783540789123
dc.identifier.urihttps://repositorio.escuelaing.edu.co/handle/001/1912
dc.description.abstractDeduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean theory and show that each of them gives rise to a Boolean decision procedure based on a canonical rewrite system modulo associativity and commutativity. Then, we present two modular extensions of our decision procedure for Dijkstra-Scholten propositional logic to the Sequent Calculus for First Order Logic and to the Syllogistic Logic with Complements of L. Moss. These extensions take the form of rewrite theories that are sound and complete for performing deduction modulo their equational parts and exhibit good mechanization properties. We illustrate the practical usefulness of this approach by a direct implementation of one of these theories in Maude rewriting logic language, and automatically proving a challenge benchmark in theorem proving.eng
dc.description.abstractDeducción con reglas de inferencia Las reglas de cálculo del módulo juegan un papel importante en la deducción automatizada como un método eficaz para escalar. Presentamos cuatro teorías ecuacionales que son isomorfas a la teoría booleana tradicional y mostramos que cada una de ellas da lugar a un procedimiento de decisión booleano basado en un sistema canónico de reescritura módulo asociatividad y conmutatividad. Luego, presentamos dos extensiones modulares de nuestro procedimiento de decisión para la lógica proposicional de Dijkstra-Scholten al Cálculo Secuente para Lógica de Primer Orden ya la Lógica Silogística con Complementos de L. Moss. Estas extensiones toman la forma de teorías de reescritura que son sólidas y completas para realizar la deducción módulo de sus partes ecuacionales y exhiben buenas propiedades de mecanización. Ilustramos la utilidad práctica de este enfoque mediante una implementación directa de una de estas teorías en Maude, reescribiendo el lenguaje lógico y demostrando automáticamente un punto de referencia de desafío en la demostración de teoremas.spa
dc.format.extent15 páginas.spa
dc.format.mimetypeapplication/pdfspa
dc.language.isoengspa
dc.publisherSpringerspa
dc.rights© Springer-Verlag Berlin Heidelberg 2008eng
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/spa
dc.sourcehttps://link.springer.com/chapter/10.1007%2F978-3-540-78913-0_25spa
dc.titleTheorem Proving Modulo Based on Boolean Equational Procedureseng
dc.typeDocumento de Conferenciaspa
dc.type.versioninfo:eu-repo/semantics/publishedVersionspa
oaire.accessrightshttp://purl.org/coar/access_right/c_14cbspa
oaire.versionhttp://purl.org/coar/version/c_970fb48d4fbd8a85spa
dc.contributor.researchgroupInformáticaspa
dc.relation.indexedN/Aspa
dc.relation.ispartofconferenceInternational Conference on Relational Methods in Computer Sciencespa
dc.relation.referencesBackhouse, R.: Program Construction: Calculating Implementations from Specifications. Willey, Chichester, UK (2003)spa
dc.relation.referencesBarendregt, H.P., Barendsen, E.: Autarkic computations and formal proofs. Journal of Automated Reasoning 28(3), 321–336 (2002)spa
dc.relation.referencesClavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)spa
dc.relation.referencesde Recherche en, L.: Informatique. The CiME System (2007), http://cime.lri.fr/spa
dc.relation.referencesDershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, ch. 6, vol. B, pp. 243–320. North-Holland, Amsterdam (1990)spa
dc.relation.referencesDijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)qspa
dc.relation.referencesDowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reasoning 31(1), 33–72 (2003)spa
dc.relation.referencesEker, S., Martí-Oliet, N., Meseguer, J., Verdejo, A.: Deduction, strategies, and rewriting. In: Martí-Oliet, N. (ed.) Proc. Strategies 2006, ENTCS, pp. 417–441. Elsevier, Amsterdam (2007)spa
dc.relation.referencesGirard, J.-Y.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)spa
dc.relation.referencesGries, D.: A calculational proof of Andrews’s challenge. Technical Report TR96-1602, Cornell University, Computer Science (August 28, 1996)spa
dc.relation.referencesGries, D., Schneider, F.B.: A Logical Approach to Discrete Math. In: Texts and Monographs in Computer Science, Springer, Heidelberg (1993)spa
dc.relation.referencesGries, D., Schneider, F.B.: Equational propositional logic. Inf. Process. Lett. 53(3), 145–152 (1995)spa
dc.relation.referencesHendrix, J., Ohsaki, H., Meseguer, J.: Sufficient completeness checking with propositional tree automata. Technical Report UIUCDCS-R-2005-2635, University of Illinois Urbana-Champaign (2005)spa
dc.relation.referencesHsiang, J.: Topics in automated theorem proving and program generation. PhD thesis, University of Illinois at Urbana-Champaign (1982)spa
dc.relation.referencesJacobson, N.: Basic algebra, vol. I. W. H. Freeman and Co., San Francisco, Calif (1974)spa
dc.relation.referencesLifschitz, V.: On calculational proofs. Ann. Pure Appl. Logic 113(1-3), 207–224 (2001)spa
dc.relation.referencesŁukasiewicz, J.: Aristotle’s Syllogistic, From the Standpoint of Modern Formal Logic. Oxford University Press, Oxford (1951)spa
dc.relation.referencesMartí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd. edn., pp. 1–87. Kluwer Academic Publishers, 2002. First published as SRI Tech. Report SRI-CSL-93-05 (August 1993)spa
dc.relation.referencesMeseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation 20(1–2), 123–160 (2007)spa
dc.relation.referencesMoss, L.S.: Syllogistic logic with complements (Draft 2007)spa
dc.relation.referencesRocha, C., Meseguer, J.: Five isomorphic Boolean theories and four equational decision procedures. Technical Report 2007-2818, University of Illinois at Urbana-Champaign (2007)spa
dc.relation.referencesRocha, C., Meseguer, J.: A rewriting decision procedure for Dijkstra-Scholten’s syllogistic logic with complements. Revista Colombiana de Computación 8(2) (2007)spa
dc.relation.referencesRocha, C., Meseguer, J.: Theorem proving modulo based on boolean equational procedures. Technical Report 2007-2922, University of Illinois at Urbana-Champaign (2007)spa
dc.relation.referencesSimmons, G.F.: Introduction to topology and modern analysis. McGraw-Hill Book Co., Inc, New York (1963)spa
dc.relation.referencesSocher-Ambrosius, R., Johann, P.: Deduction Systems. Springer, Berlin (1997)spa
dc.relation.referencesStehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic: Specifying typed higher-order languages in a first-order logical framework. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 334–375. Springer, Heidelberg (2004)spa
dc.relation.referencesViry, P.: Adventures in sequent calculus modulo equations. Electr. Notes Theor. Comput. Sci. 15 (1998)spa
dc.relation.referencesViry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)spa
dc.rights.accessrightsinfo:eu-repo/semantics/closedAccessspa
dc.rights.creativecommonsAtribución 4.0 Internacional (CC BY 4.0)spa
dc.subject.armarcProcedimiento de decisiónspa
dc.subject.armarcLógica proposicionalspa
dc.subject.armarcPrueba del teoremaspa
dc.subject.armarcTeoría Ecuacionalspa
dc.subject.armarcCálculo Secuencialspa
dc.subject.proposalDecision Procedureeng
dc.subject.proposalPropositional Logiceng
dc.subject.proposalTheorem Proveeng
dc.subject.proposalEquational Theoryeng
dc.subject.proposalSequent Calculuseng
dc.type.coarhttp://purl.org/coar/resource_type/c_f744spa
dc.type.contentTextspa
dc.type.driverinfo:eu-repo/semantics/conferenceObjectspa
dc.type.redcolhttps://purl.org/redcol/resource_type/WPspa


Ficheros en el ítem

Thumbnail

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem

© Springer-Verlag Berlin Heidelberg 2008
Excepto si se señala otra cosa, la licencia del ítem se describe como © Springer-Verlag Berlin Heidelberg 2008