Clausal Presentation of Theories in Deduction Modulo
| Autor: | Gao, Jianhua |
|---|---|
| Přispěvatelé: | Types, Logic and computing (TYPICAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), State Key Laboratory of Computer Science [Beijing] (LCS), Institute of Software Chinese Academy of Sciences [Beijing], Germain Faure, Stéphane Lengrand, Assia Mahboubi |
| Jazyk: | angličtina |
| Rok vydání: | 2011 |
| Předmět: |
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION Computer Science::Programming Languages [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing) Computer Science::Computational Complexity Computer Science::Artificial Intelligence |
| Zdroj: | PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Germain Faure, Stéphane Lengrand, Assia Mahboubi, Aug 2011, Wroclaw, Poland |
| Popis: | International audience; Resolution modulo is an extension of first-order resolution where axioms are replaced by rewrite rules, used to rewrite, or more generally narrow, clauses during the search. In the first version of this method, clauses were rewritten to arbitrary propositions, that needed to be dynamically transformed into clauses. This unpleasant feature can be eliminated when the rewrite system is clausal, i.e. when it transforms clauses to clauses. We show in this paper that how to transform any rewrite system into a clausal one, preserving the existence of cut free proof of any sequent. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|