Theorem Proving Modulo Based on Boolean Equational Procedures
Deduction 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 procedur...
- Autores:
-
Rocha, Camilo
Meseguer, José
- Tipo de recurso:
- http://purl.org/coar/resource_type/c_f744
- Fecha de publicación:
- 2008
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- eng
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/1912
- Acceso en línea:
- https://repositorio.escuelaing.edu.co/handle/001/1912
- Palabra clave:
- Procedimiento de decisión
Lógica proposicional
Prueba del teorema
Teoría Ecuacional
Cálculo Secuencial
Decision Procedure
Propositional Logic
Theorem Prove
Equational Theory
Sequent Calculus
- Rights
- closedAccess
- License
- © Springer-Verlag Berlin Heidelberg 2008
| id |
ESCUELAIG2_41b565c53a2757967f64a030c991c593 |
|---|---|
| oai_identifier_str |
oai:repositorio.escuelaing.edu.co:001/1912 |
| network_acronym_str |
ESCUELAIG2 |
| network_name_str |
Repositorio Institucional ECI |
| repository_id_str |
|
| dc.title.eng.fl_str_mv |
Theorem Proving Modulo Based on Boolean Equational Procedures |
| title |
Theorem Proving Modulo Based on Boolean Equational Procedures |
| spellingShingle |
Theorem Proving Modulo Based on Boolean Equational Procedures Procedimiento de decisión Lógica proposicional Prueba del teorema Teoría Ecuacional Cálculo Secuencial Decision Procedure Propositional Logic Theorem Prove Equational Theory Sequent Calculus |
| title_short |
Theorem Proving Modulo Based on Boolean Equational Procedures |
| title_full |
Theorem Proving Modulo Based on Boolean Equational Procedures |
| title_fullStr |
Theorem Proving Modulo Based on Boolean Equational Procedures |
| title_full_unstemmed |
Theorem Proving Modulo Based on Boolean Equational Procedures |
| title_sort |
Theorem Proving Modulo Based on Boolean Equational Procedures |
| dc.creator.fl_str_mv |
Rocha, Camilo Meseguer, José |
| dc.contributor.author.none.fl_str_mv |
Rocha, Camilo Meseguer, José |
| dc.contributor.researchgroup.spa.fl_str_mv |
Informática |
| dc.subject.armarc.spa.fl_str_mv |
Procedimiento de decisión Lógica proposicional Prueba del teorema Teoría Ecuacional Cálculo Secuencial |
| topic |
Procedimiento de decisión Lógica proposicional Prueba del teorema Teoría Ecuacional Cálculo Secuencial Decision Procedure Propositional Logic Theorem Prove Equational Theory Sequent Calculus |
| dc.subject.proposal.eng.fl_str_mv |
Decision Procedure Propositional Logic Theorem Prove Equational Theory Sequent Calculus |
| description |
Deduction 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. |
| publishDate |
2008 |
| dc.date.issued.none.fl_str_mv |
2008 |
| dc.date.accessioned.none.fl_str_mv |
2021-12-07T17:19:23Z |
| dc.date.available.none.fl_str_mv |
2021-12-07T17:19:23Z |
| dc.type.spa.fl_str_mv |
Documento de Conferencia |
| dc.type.coar.fl_str_mv |
http://purl.org/coar/resource_type/c_c94f |
| dc.type.coarversion.fl_str_mv |
http://purl.org/coar/version/c_970fb48d4fbd8a85 |
| dc.type.version.spa.fl_str_mv |
info:eu-repo/semantics/publishedVersion |
| dc.type.coar.spa.fl_str_mv |
http://purl.org/coar/resource_type/c_f744 |
| dc.type.content.spa.fl_str_mv |
Text |
| dc.type.driver.spa.fl_str_mv |
info:eu-repo/semantics/conferenceObject |
| dc.type.redcol.spa.fl_str_mv |
https://purl.org/redcol/resource_type/WP |
| format |
http://purl.org/coar/resource_type/c_f744 |
| status_str |
publishedVersion |
| dc.identifier.isbn.none.fl_str_mv |
9783540789130 9783540789123 |
| dc.identifier.uri.none.fl_str_mv |
https://repositorio.escuelaing.edu.co/handle/001/1912 |
| identifier_str_mv |
9783540789130 9783540789123 |
| url |
https://repositorio.escuelaing.edu.co/handle/001/1912 |
| dc.language.iso.spa.fl_str_mv |
eng |
| language |
eng |
| dc.relation.indexed.spa.fl_str_mv |
N/A |
| dc.relation.ispartofconference.spa.fl_str_mv |
International Conference on Relational Methods in Computer Science |
| dc.relation.references.spa.fl_str_mv |
Backhouse, R.: Program Construction: Calculating Implementations from Specifications. Willey, Chichester, UK (2003) Barendregt, H.P., Barendsen, E.: Autarkic computations and formal proofs. Journal of Automated Reasoning 28(3), 321–336 (2002) Clavel, 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) de Recherche en, L.: Informatique. The CiME System (2007), http://cime.lri.fr/ Dershowitz, 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) Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)q Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reasoning 31(1), 33–72 (2003) Eker, 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) Girard, J.-Y.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989) Gries, D.: A calculational proof of Andrews’s challenge. Technical Report TR96-1602, Cornell University, Computer Science (August 28, 1996) Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. In: Texts and Monographs in Computer Science, Springer, Heidelberg (1993) Gries, D., Schneider, F.B.: Equational propositional logic. Inf. Process. Lett. 53(3), 145–152 (1995) Hendrix, J., Ohsaki, H., Meseguer, J.: Sufficient completeness checking with propositional tree automata. Technical Report UIUCDCS-R-2005-2635, University of Illinois Urbana-Champaign (2005) Hsiang, J.: Topics in automated theorem proving and program generation. PhD thesis, University of Illinois at Urbana-Champaign (1982) Jacobson, N.: Basic algebra, vol. I. W. H. Freeman and Co., San Francisco, Calif (1974) Lifschitz, V.: On calculational proofs. Ann. Pure Appl. Logic 113(1-3), 207–224 (2001) Łukasiewicz, J.: Aristotle’s Syllogistic, From the Standpoint of Modern Formal Logic. Oxford University Press, Oxford (1951) Martí-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) Meseguer, 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) Moss, L.S.: Syllogistic logic with complements (Draft 2007) Rocha, C., Meseguer, J.: Five isomorphic Boolean theories and four equational decision procedures. Technical Report 2007-2818, University of Illinois at Urbana-Champaign (2007) Rocha, C., Meseguer, J.: A rewriting decision procedure for Dijkstra-Scholten’s syllogistic logic with complements. Revista Colombiana de Computación 8(2) (2007) Rocha, C., Meseguer, J.: Theorem proving modulo based on boolean equational procedures. Technical Report 2007-2922, University of Illinois at Urbana-Champaign (2007) Simmons, G.F.: Introduction to topology and modern analysis. McGraw-Hill Book Co., Inc, New York (1963) Socher-Ambrosius, R., Johann, P.: Deduction Systems. Springer, Berlin (1997) Stehr, 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) Viry, P.: Adventures in sequent calculus modulo equations. Electr. Notes Theor. Comput. Sci. 15 (1998) Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002) |
| dc.rights.eng.fl_str_mv |
© Springer-Verlag Berlin Heidelberg 2008 |
| dc.rights.coar.fl_str_mv |
http://purl.org/coar/access_right/c_14cb |
| dc.rights.uri.spa.fl_str_mv |
https://creativecommons.org/licenses/by/4.0/ |
| dc.rights.accessrights.spa.fl_str_mv |
info:eu-repo/semantics/closedAccess |
| dc.rights.creativecommons.spa.fl_str_mv |
Atribución 4.0 Internacional (CC BY 4.0) |
| rights_invalid_str_mv |
© Springer-Verlag Berlin Heidelberg 2008 https://creativecommons.org/licenses/by/4.0/ Atribución 4.0 Internacional (CC BY 4.0) http://purl.org/coar/access_right/c_14cb |
| eu_rights_str_mv |
closedAccess |
| dc.format.extent.spa.fl_str_mv |
15 páginas. |
| dc.format.mimetype.spa.fl_str_mv |
application/pdf |
| dc.publisher.spa.fl_str_mv |
Springer |
| dc.source.spa.fl_str_mv |
https://link.springer.com/chapter/10.1007%2F978-3-540-78913-0_25 |
| institution |
Escuela Colombiana de Ingeniería Julio Garavito |
| bitstream.url.fl_str_mv |
https://repositorio.escuelaing.edu.co/bitstream/001/1912/5/Theorem%20Proving%20Modulo%20Based%20on%20Boolean%20Equational%20Procedures.pdf.txt https://repositorio.escuelaing.edu.co/bitstream/001/1912/4/Theorem%20Proving%20Modulo%20Based%20on%20Boolean%20Equational%20Procedures.png https://repositorio.escuelaing.edu.co/bitstream/001/1912/6/Theorem%20Proving%20Modulo%20Based%20on%20Boolean%20Equational%20Procedures.pdf.jpg https://repositorio.escuelaing.edu.co/bitstream/001/1912/3/Theorem%20Proving%20Modulo%20Based%20on%20Boolean%20Equational%20Procedures.pdf https://repositorio.escuelaing.edu.co/bitstream/001/1912/2/license.txt |
| bitstream.checksum.fl_str_mv |
5e4800d5f95ee3d2303ae21c5f3a16fd c9a06dd8bc5ac909ad7edef7835ae486 9aafba12748dfbd9d6f40b0394eaffaa aa5479b25fa21713face6d7de0082f0e 5a7ca94c2e5326ee169f979d71d0f06e |
| bitstream.checksumAlgorithm.fl_str_mv |
MD5 MD5 MD5 MD5 MD5 |
| repository.name.fl_str_mv |
Repositorio Escuela Colombiana de Ingeniería Julio Garavito |
| repository.mail.fl_str_mv |
repositorio.eci@escuelaing.edu.co |
| _version_ |
1814355606212968448 |
| spelling |
Rocha, Camilo649eba80a4c919beefa7d19955bc2950600Meseguer, José6da02984a567cfba226ed9b8bf7c47c0600Informática2021-12-07T17:19:23Z2021-12-07T17:19:23Z200897835407891309783540789123https://repositorio.escuelaing.edu.co/handle/001/1912Deduction 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.Deducció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.15 páginas.application/pdfengSpringer© Springer-Verlag Berlin Heidelberg 2008https://creativecommons.org/licenses/by/4.0/info:eu-repo/semantics/closedAccessAtribución 4.0 Internacional (CC BY 4.0)http://purl.org/coar/access_right/c_14cbhttps://link.springer.com/chapter/10.1007%2F978-3-540-78913-0_25Theorem Proving Modulo Based on Boolean Equational ProceduresDocumento de Conferenciainfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_f744http://purl.org/coar/resource_type/c_c94fTextinfo:eu-repo/semantics/conferenceObjecthttps://purl.org/redcol/resource_type/WPhttp://purl.org/coar/version/c_970fb48d4fbd8a85N/AInternational Conference on Relational Methods in Computer ScienceBackhouse, R.: Program Construction: Calculating Implementations from Specifications. Willey, Chichester, UK (2003)Barendregt, H.P., Barendsen, E.: Autarkic computations and formal proofs. Journal of Automated Reasoning 28(3), 321–336 (2002)Clavel, 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)de Recherche en, L.: Informatique. The CiME System (2007), http://cime.lri.fr/Dershowitz, 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)Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)qDowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reasoning 31(1), 33–72 (2003)Eker, 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)Girard, J.-Y.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)Gries, D.: A calculational proof of Andrews’s challenge. Technical Report TR96-1602, Cornell University, Computer Science (August 28, 1996)Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. In: Texts and Monographs in Computer Science, Springer, Heidelberg (1993)Gries, D., Schneider, F.B.: Equational propositional logic. Inf. Process. Lett. 53(3), 145–152 (1995)Hendrix, J., Ohsaki, H., Meseguer, J.: Sufficient completeness checking with propositional tree automata. Technical Report UIUCDCS-R-2005-2635, University of Illinois Urbana-Champaign (2005)Hsiang, J.: Topics in automated theorem proving and program generation. PhD thesis, University of Illinois at Urbana-Champaign (1982)Jacobson, N.: Basic algebra, vol. I. W. H. Freeman and Co., San Francisco, Calif (1974)Lifschitz, V.: On calculational proofs. Ann. Pure Appl. Logic 113(1-3), 207–224 (2001)Łukasiewicz, J.: Aristotle’s Syllogistic, From the Standpoint of Modern Formal Logic. Oxford University Press, Oxford (1951)Martí-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)Meseguer, 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)Moss, L.S.: Syllogistic logic with complements (Draft 2007)Rocha, C., Meseguer, J.: Five isomorphic Boolean theories and four equational decision procedures. Technical Report 2007-2818, University of Illinois at Urbana-Champaign (2007)Rocha, C., Meseguer, J.: A rewriting decision procedure for Dijkstra-Scholten’s syllogistic logic with complements. Revista Colombiana de Computación 8(2) (2007)Rocha, C., Meseguer, J.: Theorem proving modulo based on boolean equational procedures. Technical Report 2007-2922, University of Illinois at Urbana-Champaign (2007)Simmons, G.F.: Introduction to topology and modern analysis. McGraw-Hill Book Co., Inc, New York (1963)Socher-Ambrosius, R., Johann, P.: Deduction Systems. Springer, Berlin (1997)Stehr, 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)Viry, P.: Adventures in sequent calculus modulo equations. Electr. Notes Theor. Comput. Sci. 15 (1998)Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)Procedimiento de decisiónLógica proposicionalPrueba del teoremaTeoría EcuacionalCálculo SecuencialDecision ProcedurePropositional LogicTheorem ProveEquational TheorySequent CalculusTEXTTheorem Proving Modulo Based on Boolean Equational Procedures.pdf.txtTheorem Proving Modulo Based on Boolean Equational Procedures.pdf.txtExtracted texttext/plain42081https://repositorio.escuelaing.edu.co/bitstream/001/1912/5/Theorem%20Proving%20Modulo%20Based%20on%20Boolean%20Equational%20Procedures.pdf.txt5e4800d5f95ee3d2303ae21c5f3a16fdMD55metadata only accessTHUMBNAILTheorem Proving Modulo Based on Boolean Equational Procedures.pngTheorem Proving Modulo Based on Boolean Equational Procedures.pngimage/png121545https://repositorio.escuelaing.edu.co/bitstream/001/1912/4/Theorem%20Proving%20Modulo%20Based%20on%20Boolean%20Equational%20Procedures.pngc9a06dd8bc5ac909ad7edef7835ae486MD54open accessTheorem Proving Modulo Based on Boolean Equational Procedures.pdf.jpgTheorem Proving Modulo Based on Boolean Equational Procedures.pdf.jpgGenerated Thumbnailimage/jpeg10702https://repositorio.escuelaing.edu.co/bitstream/001/1912/6/Theorem%20Proving%20Modulo%20Based%20on%20Boolean%20Equational%20Procedures.pdf.jpg9aafba12748dfbd9d6f40b0394eaffaaMD56metadata only accessORIGINALTheorem Proving Modulo Based on Boolean Equational Procedures.pdfTheorem Proving Modulo Based on Boolean Equational Procedures.pdfDocumento de Conferenciaapplication/pdf799871https://repositorio.escuelaing.edu.co/bitstream/001/1912/3/Theorem%20Proving%20Modulo%20Based%20on%20Boolean%20Equational%20Procedures.pdfaa5479b25fa21713face6d7de0082f0eMD53metadata only accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1912/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open access001/1912oai:repositorio.escuelaing.edu.co:001/19122022-11-22 03:00:54.655metadata only accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK |