Výsledky vyhledávání - "Germain Faure"

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Autor: Chantal Keller, Benjamin Grégoire, Benjamin Werner, Germain Faure, Laurent Théry, Michael Armand

Publikováno v: CPP-Certified Programs and Proofs-First International Conference-2011
CPP-Certified Programs and Proofs-First International Conference-2011, Dec 2011, Kenting, Taiwan. pp.135-150, ⟨10.1007/978-3-642-25379-9_12⟩
Certified Programs and Proofs ISBN: 9783642253782
CPP

International audience; We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::193a32fd8306ade1a67d887f6e80c01f
https://hal.inria.fr/hal-00639130

Zobrazit plný text záznamu

SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers

Autor: Germain Faure, Robert Nieuwenhuis, Enric Rodríguez-Carbonell, Albert Oliveras

Publikováno v: Theory and Applications of Satisfiability Testing-SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings
Theory and Applications of Satisfiability Testing-SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings, Springer, 2008, 4996, pp.77-90
Theory and Applications of Satisfiability Testing – SAT 2008 ISBN: 9783540797180
SAT

International audience; Many highly sophisticated tools exist for solving linear arith- metic optimization and feasibility problems. Here we analyze why it is difficult to use these tools inside systems for SAT Modulo Theories (SMT) for linear arithm

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cba1a366e092712451b1ad2114c3b8c2
https://hal.inria.fr/inria-00358813/document

Zobrazit plný text záznamu

Confluence of Pattern-Based Calculi

Autor: Horatiu Cirstea, Germain Faure

Publikováno v: Lecture Notes in Computer Science ISBN: 9783540734475
RTA
18th International Conference on Term Rewriting and Applications-RTA 2007
18th International Conference on Term Rewriting and Applications-RTA 2007, Jun 2007, Paris, France. pp.78-92, ⟨10.1007/978-3-540-73449-9_8⟩

International audience; Different pattern calculi integrate the functional mechanisms from the lambda-calculus and the matching capabilities from rewriting. Several approaches are used to obtain the confluence but in practice the proof methods share

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f011b5b848a755dd0d075f6596464aa3
https://doi.org/10.1007/978-3-540-73449-9_8

Zobrazit plný text záznamu

A Rho-Calculus of explicit constraint application

Autor: Horatiu Cirstea, Germain Faure, Claude Kirchner

Publikováno v: Higher-Order and Symbolic Computation
Higher-Order and Symbolic Computation, 2007, Special Issue on Rewriting Logic and its Applications, 20, pp.37-72. ⟨10.1007/s10990-007-9004-2⟩
Workshop on Rewriting Logic and Applications
Workshop on Rewriting Logic and Applications, Mar 2004, Barcelona (Spain), Spain
WRLA
Higher-Order and Symbolic Computation, Springer Verlag, 2007, Special Issue on Rewriting Logic and its Applications, 20, pp.37-72. ⟨10.1007/s10990-007-9004-2⟩

International audience; Theoretical presentations of the rho-calculus often treat the matching constraint computations as an atomic operation although matching constraints are explicitly expressed. Actual implementations have to take a much more real

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9e28644f44bb32179d6f754b1a2f64da
https://inria.hal.science/inria-00000628v3/file/paper.pdf

Zobrazit plný text záznamu

From functional programs to interaction nets via the Rewriting Calculus

Autor: Horatiu Cirstea, Germain Faure, Ian Mackie, Maribel Fernández, François-Régis Sinot

Publikováno v: Sixth International Workshop on Reduction Strategies in Rewriting and Programming
Sixth International Workshop on Reduction Strategies in Rewriting and Programming, Aug 2006, Seattle, Washington, United States. pp.39-56

We use the ρ-calculus as an intermediate language to compile functional languages with pattern-matching features, and give an interaction net encoding of the ρ-terms arising from the compilation. This encoding gives rise to new strategies of evalua

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::506c7f1f81a503e45d5284f67d4d6f9c
https://hal.inria.fr/inria-00000821

Zobrazit plný text záznamu

Matching Modulo Superdevelopments Application to Second-Order Matching

Autor: Germain Faure

Publikováno v: Logic for Programming, Artificial Intelligence, and Reasoning ISBN: 9783540482819
LPAR

To perform higher-order matching, we need to decide the βη-equivalence on λ-terms. The first way to do it is to use simply typed λ-calculus and this is the usual framework where higher-order matching is performed. Another approach consists in dec

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::4fd7a3f4e92b88269f1ce9c9a3b8a363
https://doi.org/10.1007/11916277_5

Zobrazit plný text záznamu

Exceptions in the rewriting calculus

Autor: Claude Kirchner, Germain Faure

Publikováno v: 13th International Conference on Rewriting Techniques and Applications-RTA 2002
13th International Conference on Rewriting Techniques and Applications-RTA 2002, Jul 2002, Copenhagen/Denmark, pp.66--82
Rewriting Techniques and Applications ISBN: 9783540439165
RTA

In the context of the rewriting calculus, we introduce and study an exception mechanism that allows us to express in a simple way rewriting strategies and that is therefore also useful for expressing theorem proving tactics. The proposed exception me

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2dca51c5673448aa7fbef9fd60682d30
https://hal.inria.fr/inria-00101011

Zobrazit plný text záznamu

Akademický článek

A ρ-calculus of explicit constraint application.

Autor: Horatiu Cirstea, Germain Faure, Claude Kirchner

Publikováno v: Higher-Order & Symbolic Computation; Jun2007, Vol. 20 Issue 1/2, p37-72, 36p

Zobrazit plný text záznamu

Verifying SAT and SMT in Coq for a fully automated decision procedure

Autor: Armand, Mickaël, Faure, Germain, Grégoire, Benjamin, Keller, Chantal, Théry, Laurent, Wener, Benjamin

Publikováno v: 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

International audience; Enjoying the power of SAT and SMT solvers in the Coq proof as- sistant without compromising soundness requires more than a yes/no answer from them. SAT and SMT solvers should also return a proof witness that can be checked by

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::72e05b6b9451ee6b30e1fef987e3abb4
https://hal.inria.fr/inria-00614041/document

Zobrazit plný text záznamu

Clausal Presentation of Theories in Deduction Modulo

Autor: Gao, Jianhua

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 re

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______165::2a8fe22e04e0731af4c2b68b136db1a2
https://inria.hal.science/inria-00614251/file/Gao.pdf

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání