Skip to Main content Skip to Navigation

inria-00072840v1  Reports
Horatiu CirsteaClaude Kirchner. Introduction to the Rewriting Calculus
[Research Report] RR-3818, INRIA. 1999, pp.50
inria-00077199v1  Reports
Gilles DowekThérèse HardinClaude Kirchner. Theorem Proving Modulo
[Research Report] RR-3400, INRIA. 1998, pp.27
inria-00138195v3  Conference papers
Guillaume Burel. Unbounded Proof-Length Speed-up in Deduction Modulo
16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Jacques Duparc, Sep 2007, Lausanne, Switzerland. pp.496-511, ⟨10.1007/978-3-540-74915-8_37⟩
inria-00001205v1  Conference papers
Sébastien Hinderer. Certification of Termination Proofs Using Polynomial Interpretations
17th European Summer School in Logic, Language and Information - ESSLLI '05, Aug 2005, Edimbourg/Grande Bretagne
hal-00531242v3  Journal articles
yves GuiraudPhilippe Malbos. Higher-dimensional normalisation strategies for acyclicity
Advances in Mathematics, Elsevier, 2012, 231 (3-4), pp.2294-2351. ⟨10.1016/j.aim.2012.05.010⟩
inria-00161092v1  Conference papers
Frédéric Blanqui. Computability Closure: Ten Years Later
Colloquium in honor of Jean-Pierre Jouannaud, Jun 2007, Cachan, France. ⟨10.1007/978-3-540-73147-4_4⟩
hal-02101787v1  Reports
Judicael Courant. Proof reconstruction (preliminary version).
[Research Report] LIP 1996-26, Laboratoire de l'informatique du parallélisme. 1996, 2+14p
hal-00484871v4  Conference papers
Thomas BraibantDamien Pous. Tactics for Reasoning modulo AC in Coq
Certified Proofs and Programs, 2011, Taiwan. pp167-182, ⟨10.1007/978-3-642-25379-9_14⟩
inria-00397689v1  Conference papers
Frédéric BlanquiCody Roux. On the relation between sized-types based termination and semantic labelling
18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal
inria-00555008v1  Journal articles
Sho SuzukiKeiichirou KusakariFrédéric Blanqui. Argument filterings and usable rules in higher-order rewrite systems
IPSJ Transactions on Programming, IPSJ, 2011, 4 (2), pp.1-12
hal-03279749v1  Conference papers
Frédéric BlanquiGilles DowekÉmilie GrienenbergerGabriel HondetFrançois Thiré. Some Axioms for Mathematics
FSCD 2021 - 6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires / Virtual, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.20⟩
hal-03044338v1  Conference papers
Beniamino AccattoliClaudia FaggianGiulio Guerrieri. Factorize Factorization
CSL 2021 - 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana, Slovenia. ⟨10.4230/LIPIcs.CSL.2021.22⟩
inria-00098426v1  Conference papers
Paliath NarendranMichaël RusinowitchRakesh Verma. RPO constraint solving is in NP
Computer Science Logic, 1998, Brno, Tchêquie, 12 p
inria-00100532v1  Journal articles
Horatiu CirsteaClaude Kirchner. The Rewriting Calculus - Part II
Logic Journal of the IGPL, Oxford University Press (OUP), 2001, 9 (3), pp.465-498. ⟨10.1093/jigpal/9.3.377⟩
inria-00101024v1  Conference papers
Eric DeplagneClaude Kirchner. Deduction versus Computation: the Case of Induction
Sixth International Conference on Artificial Intelligence and Symbolic Computation - AISC'2002, Jul 2002, Marseille, France, pp.4-6
inria-00099654v1  Journal articles
Olivier FissoreIsabelle GnaedigHélène Kirchner. Outermost ground termination
Electronic Notes in Theoretical Computer Science, Elsevier, 2003, 71, 20 p
inria-00099932v1  Reports
Frédéric Blanqui. Prototype d'extension du système Coq
[Contrat] A04-R-505 || blanqui04e, 2004, 8 p
inria-00100025v1  Conference papers
Horatiu CirsteaPierre-Etienne MoreauAntoine Reilles. Rule based programming in Java for protocol verification
5th International Workshop on Rewriting Logic and its Applications - WRLA'2004, Narciso Marti-Oliet, 2004, Barcelona, Spain, 18 p
inria-00099930v1  Reports
Frédéric Blanqui. Définition de la classe de réécriture à intégrer
[Contrat] A04-R-487 || blanqui04c, 2004, 7 p
inria-00099700v1  Conference papers
Abdessamad IminePascal MolliGérald OsterPascal Urso. VOTE: Group Editors Analyzing Tool
Fourth International Workshop on First-Order Theorem Proving - FTP'03, 2003, Valencia, Spain, pp.153-161, ⟨10.1016/S1571-0661(04)80660-1⟩
inria-00098575v1  Conference papers
Hélène Touzet. Encoding the Hydra battle as a rewrite system
International Symposium on the Mathematical Foundations of Computer Science - MFCS'98, Aug 1998, Brno, Czech Republic, pp.267-276
inria-00098607v1  Conference papers
Rakesh VermaMichaël RusinowitchDenis Lugiez. Algorithms and Reductions for Rewriting Problems
Proceedings 9th Conference on Rewriting Techniques and Applications, 1998, Tsukuba, Japan, pp.166-180
inria-00099059v1  Conference papers
Hélène KirchnerIsabelle Gnaedig. Termination and normalisation under strategies--Proofs in ELAN
3rd International Workshop on Rewriting Logic & Applications - WRLA'2000, 2000, Kanazawa, Japan, pp.93--115
inria-00099867v1  Reports
Olivier BournezFlorent Garnier. Proving Positive Almost-Sure Termination
[Intern report] A04-R-409 || bournez04h, 2004, 16 p
inria-00099386v1  Conference papers
Christophe Ringeissen. Handling Relations over Finite Domains in the Rule-Based System ELAN
Third International Workshop on Rewriting Logic & Applications - WRLA'2000, 2000, Kanazawa, Japon, 17 p