Výsledky vyhledávání - "Clément Houtmann"

Akademický článek

Superdeduction in Lambda-Bar-Mu-Mu-Tilde

Autor: Clément Houtmann

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 47, Iss Proc. CL&C 2010, Pp 34-43 (2011)

Superdeduction is a method specially designed to ease the use of first-order theories in predicate logic. The theory is used to enrich the deduction system with new deduction rules in a systematic, correct and complete way. A proof-term language and

Externí odkaz: https://doaj.org/article/66579203a1a04915a360fe6704376f96

Zobrazit plný text záznamu

Strong normalisation in two Pure Pattern Type Systems

Autor: Benjamin Wack, Clément Houtmann

Publikováno v: Mathematical Structures in Computer Science
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2008, Rewriting calculi, higher-order reductions and patterns, 18 (3), pp.431-465. ⟨10.1017/S0960129508006749⟩
Mathematical Structures in Computer Science, 2008, Rewriting calculi, higher-order reductions and patterns, 18 (3), pp.431-465. ⟨10.1017/S0960129508006749⟩

Pure Pattern Type Systems (P2TS) combine the frameworks and capabilities of rewriting and λ-calculus within a unified setting. Their type systems, which are adapted from Barendregt's λ-cube, are especially interesting from a logical point of view.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4ad3c39a2684056d6ab7e51058cd7760
https://doi.org/10.1017/s0960129508006749

Zobrazit plný text záznamu

Orthogonality and Boolean Algebras for Deduction Modulo

Autor: Aloïs Brunel, Olivier Hermant, Clément Houtmann

Publikováno v: Lecture Notes in Computer Science ISBN: 9783642216909
TLCA

Originating from automated theorem proving, deduction modulo removes computational arguments from proofs by interleaving rewriting with the deduction process. From a proof-theoretic point of view, deduction modulo defines a generic notion of cut that

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::6c8e79fef8a9bb2ec7971ca0f70c342b
https://doi.org/10.1007/978-3-642-21691-6_9

Zobrazit plný text záznamu

Superdeduction in Lambda-bar-mu-mu-tilde

Autor: Clément Houtmann

Publikováno v: Classical Logic and Computation 2010
Classical Logic and Computation 2010, Aug 2010, Brno, Czech Republic. pp.33-43, ⟨10.4204/EPTCS.47.5⟩
Electronic Proceedings in Theoretical Computer Science, Vol 47, Iss Proc. CL&C 2010, Pp 34-43 (2011)
CL&C

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::40e9d7b40c9148e17134c40387158647
https://hal.inria.fr/inria-00498744

Zobrazit plný text záznamu

Axiom directed Focusing

Autor: Clément Houtmann

Publikováno v: Types for Proofs and Programs, International Conference, TYPES 2008
Types for Proofs and Programs, International Conference, TYPES 2008, Mar 2008, Torino, Italy. pp.169-185, ⟨10.1007/978-3-642-02444-3_11⟩
Lecture Notes in Computer Science ISBN: 9783642024436
TYPES

Long version; International audience; Superdeduction and deduction modulo are methods specially designed to ease the use of first-order theories in predicate logic. Superdeduction modulo, which combines both, enables the user to make a distinct use o

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e4463ea79732d13f749ed48ada0e4ff2
https://inria.hal.science/inria-00212059

Zobrazit plný text záznamu

Superdeduction at Work

Autor: Paul Brauner, Claude Kirchner, Clément Houtmann

Publikováno v: Rewriting, Computation and Proof ISBN: 9783540731467
Rewriting, Computation and Proof
Colloquium in honor of Jean-Pierre Jouannaud
Colloquium in honor of Jean-Pierre Jouannaud, Jun 2007, Cachan, France. pp.132-166, ⟨10.1007/978-3-540-73147-4⟩

International audience; Superdeduction is a systematic way to extend a deduction system like the sequent calculus by new deduction rules computed from the user theory. We show how this could be done in a systematic, correct and complete way. We prove

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1660ba812b49e96b037929fd3603cf84
https://doi.org/10.1007/978-3-540-73147-4_7

Zobrazit plný text záznamu

Principles of Superdeduction

Autor: Clément Houtmann, Claude Kirchner, Paul Brauner

Publikováno v: LICS
Twenty-Second Annual IEEE Symposium on Logic in Computer Science-LiCS 2007
Twenty-Second Annual IEEE Symposium on Logic in Computer Science-LiCS 2007, Jul 2007, Wroclaw, Poland. ⟨10.1109/LICS.2007.37⟩

International audience; In predicate logic, the proof that a theorem P holds in a theory Th is typically conducted in natural deduction or in the sequent calculus using all the information contained in the theory in a uniform way. Introduced ten year

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::afd4419c917d0ecfa3d495e743ff0dee
https://doi.org/10.1109/lics.2007.37

Zobrazit plný text záznamu

Distributive Rho-Calculus

Autor: Horatiu Cirstea, Clément Houtmann, Benjamin Wack

Publikováno v: WRLA 2006
WRLA 2006, Apr 2006, Vienna, Austria. pp.29, ⟨10.1016/j.entcs.2007.06.010⟩
WRLA

International audience; The rewriting calculus has been introduced as a general formalism that uniformly integrates rewriting and lambda-calculus. In this calculus all the basic ingredients of rewriting such as rewrite rules, rule applications and re

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4ae1399bffa91a4cf0e76524d0c0ed7b
https://inria.hal.science/inria-00001112

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání