Search

Your search keyword '"Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)"' showing total 56 results
Start Over Author "Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)" Topic theoryofcomputation_logicsandmeaningsofprograms
56 results on '"Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)"'

1. ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti

Author

Raphaël Cauderlier, Catherine Dubois, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), Centre d'enseignement Cnam Paris (CNAM Paris), Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Deduction modulo, interopérabilité et démonstration automatique ( DEDUCTEAM ), 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 ), Conservatoire National des Arts et Métiers - Paris ( CNAM Paris ), Conservatoire National des Arts et Métiers [CNAM] ( CNAM ), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise ( ENSIIE ), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification [Cachan] (LSV), and École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Recursion, Programming language, Modulo, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Extension (predicate logic), computer.software_genre, Mathematical proof, 01 natural sciences, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0202 electrical engineering, electronic engineering, information engineering, [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO], Compiler, Rewriting, Pattern matching, computer, Mathematics
Abstract

International audience; The programming environment FoCaLiZe allows the user to specify, implement, and prove programs with the help of the theorem prover Zenon. In the actual version, those proofs are verified by Coq. In this paper we propose to extend the FoCaLiZe compiler by a backend to the Dedukti language in order to benefit from Zenon Modulo, an extension of Zenon for Deduction modulo. By doing so, FoCaLiZe can benefit from a technique for finding and verifying proofs more quickly. The paper focuses mainly on the process that overcomes the lack of local pattern-matching and recursive definitions in Dedukti.

Published
2016
Full Text
View/download PDF

2. Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Author

Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Shenzhen University [Shenzhen]

Subjects
decreasing diagrams, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Mathematics (miscellaneous), orthogonal reductions, Computer Science::Logic in Computer Science, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Church-Rosser property, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], nested critical pairs, Confluence, Computer Science Applications
Abstract

User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom’s decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, confluence of a terminating set of left-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. The present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pairs. The rewrite relation used for analyzing confluence may rewrite arbitrarily many non-overlapping redexes in a single step. This relation gives rise to critical pairs that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. Practical examples of use of this technique are analyzed.

Published
2022
Full Text
View/download PDF

3. Compositional pre-processing for automated reasoning in dependent type theory

Author

Blot, Valentin, Cousineau, Denis, Crance, Enzo, de Prisque, Louise Dubois, Keller, Chantal, Mahboubi, Assia, Vial, Pierre, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Mitsubishi Electric R&D Centre Europe [France] (MERCE-France), Mitsubishi Electric [France], Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-École Centrale de Nantes (Nantes Univ - ECN), Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST), Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Nantes Université (Nantes Univ), Laboratoire des Sciences du Numérique de Nantes (LS2N), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Calculus of Inductive Constructions, Interactive theorem proving, Arithmetic, Higher order logic, Type theory, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Automated reasoning, Pre-processing, Logic in Computer Science (cs.LO), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Coq
Abstract

International audience; In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of pre-processing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines.

Published
2023
Full Text
View/download PDF

4. A direct computational interpretation of second-order arithmetic via update recursion

Author

Blot, Valentin, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; Second-order arithmetic has two kinds of computational interpretations: via Spector's bar recursion of via Girard's polymorphic lambda-calculus. Bar recursion interprets the negative translation of the axiom of choice which, combined with an interpretation of the negative translation of the excluded middle, gives a computational interpretation of the negative translation of the axiom scheme of comprehension. It is then possible to instantiate universally quantified sets with arbitrary formulas (second-order elimination). On the other hand, polymorphic lambda-calculus interprets directly second-order elimination by means of polymorphic types. The present work aims at bridging the gap between these two interpretations by interpreting directly second-order elimination through update recursion, which is a variant of bar recursion.

Published
2022
Full Text
View/download PDF

5. Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting

Author

Michael Färber, University of Innsbruck, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Leopold Franzens Universität Innsbruck - University of Innsbruck

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, reduction, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Dedukti, type checking, 0202 electrical engineering, electronic engineering, information engineering, concurrency, Interactive proof systems, CCS Concepts: • Theory of computation → Logic and verification, Equational logic and rewriting, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Automated reasoning, Higher order logic concurrency, Logic in Computer Science (cs.LO), rewriting, sharing, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Rust, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, verification, performance
Abstract

Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today's small proof checkers either does not support concurrency at all or only limited forms thereof, restricting the efficiency of proof checking on multi-core processors. This work shows the design of a small, memory- and thread-safe kernel that efficiently checks proofs both concurrently and non-concurrently. This design is implemented in a new proof checker called Kontroli for the lambda-Pi calculus modulo rewriting, which is an established framework to uniformly express a multitude of logical systems. Kontroli is faster than the reference proof checker for this calculus, Dedukti, on all of five evaluated datasets obtained from proof assistants and interactive theorem provers. Furthermore, Kontroli reduces the time of the most time-consuming part of proof checking using eight threads by up to 6.6x., 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '22), Jan 2022, Philadelphia, PA, United States

Published
2022
Full Text
View/download PDF

6. Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity

Author

Blanqui, Frédéric, Centre National de la Recherche Scientifique (CNRS), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], type universes, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], rewriting theory, Theory of computation → Type theory, Theory of computation → Logic, rewriting, associativity and commutativity, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, logical framework, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, type theory, Theory of computation → Equational logic and rewriting
Abstract

The encoding of proof systems and type theories in logical frameworks is key to allow the translation of proofs from one system to the other. The λΠ-calculus modulo rewriting is a powerful logical framework in which various systems have already been encoded, including type systems with an infinite hierarchy of type universes equipped with a unary successor operator and a binary max operator: Matita, Coq, Agda and Lean. However, to decide the word problem in this max-successor algebra, all the encodings proposed so far use rewriting with matching modulo associativity and commutativity (AC), which is of high complexity and difficult to integrate in usual algorithms for b-reduction and type-checking. In this paper, we show that we do not need matching modulo AC by enforcing terms to be in some special canonical form wrt associativity and commutativity, and by using rewriting rules taking advantage of this canonical form. This work has been implemented in the proof assistant Lambdapi., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 24:1-24:14

Published
2022
Full Text
View/download PDF

7. Unification of drags and confluence of drag rewriting

Author

Jouannaud, Jean-Pierre, Orejas, Fernando, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Universitat Politècnica de Catalunya [Barcelona] (UPC), Jouannaud, Jean-Pierre, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), Laboratoire de Méthodes Formelles, Université de Paris-Saclay, Université de Paris Saclay, Universitat Politècnica de Catalunya. Departament de Ciències de la Computació, and Universitat Politècnica de Catalunya. ALBCOM - Algorísmia, Bioinformàtica, Complexitat i Mètodes Formals

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], unification, InformationSystems_INFORMATIONINTERFACESANDPRESENTATION(e.g.,HCI), Logic, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], GeneralLiterature_MISCELLANEOUS, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Theoretical Computer Science, Physics::Fluid Dynamics, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Drags, Algorismes computacionals, ComputingMethodologies_COMPUTERGRAPHICS, graphs, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Confluence, ACM: D.: Software, Computer algorithms, ACM: F.: Theory of Computation, Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat [Àrees temàtiques de la UPC], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, Unification, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, confluence, Computer Science::Programming Languages, Astrophysics::Earth and Planetary Astrophysics, Graphs, Software
Abstract

Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules. This work is partially supported by MCIN/AEI /10.13039/501100011033 under grant PID2020-112581GB-C21.

Published
2023
Full Text
View/download PDF

8. Representing Agda and coinduction in the λΠ-calculus modulo rewriting

Author

Felicissimo, Thiago, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), LSV, ENS Paris Saclay, Université Paris-Saclay, Frederic Blanqui, and Gilles Dowek

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; Coinduction is a principle, or a proof technique, dual to induction and which allows to handle possibly infinite objects in a natural way, such as infinite lists, infinite trees, formal languages, non well-founded sets, etc. Because of its usefulness, it is increasingly being added to proof assistants, such as Coq, Isabelle, PVS and Agda. In order to be able to translate proofs by coinduction coming from multiple proof assistants it is thus important to first understand how to encode coinduction in Dedukti, a problem that had never been addressed before. During this internship, we studied the representation of Agda and coinduction in Dedukti. Among the techniques of implementing coinduction in proof assistants, Agda features two presentations: musical coinduction and copattern coinduction. Based on their internal syntax representation in Agda, we proposed an encoding of both presentations in Dedukti. We resumed the development of the Agda2Dedukti translator and extended it with the proposed encoding, allowing it to translate automatically proofs by coinduction into Dedukti.

Published
2021

9. Confluence in UnTyped Higher-Order Theories by means of Critical Pairs

Author

Férey, Gaspard, Jouannaud, Jean-Pierre, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Church-Rosser property, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Confluence, Type systems, [INFO]Computer Science [cs], Ancestor peaks, Critical peaks, Decreasing diagrams, Lambda calculus
Abstract

User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. We develop here techniques that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. The present paper concentrates on the case where rewrite rules are left-linear and critical pairs can be joined without using beta-rewrite steps. The other two cases will be addressed in forthcoming papers.

Published
2021

10. Small, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting

Author

Färber, Michael, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
sharing, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, type checking, Rust, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], reduction, concurrency, verification, Dedukti, performance, rewriting
Abstract

Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today's small proof checkers either does not support concurrency at all or only limited forms thereof, restricting the efficiency of proof checking on multi-core processors. This work presents a small proof checker with support for concurrent proof checking, achieving state-of-the-art performance in both concurrent and nonconcurrent settings. The proof checker implements the lambda-Pi calculus modulo rewriting, which is an established framework to uniformly express a multitude of logical systems. The proof checker is faster than the reference proof checker for this calculus, Dedukti, on all of five evaluated datasets obtained from proof assistants and interactive theorem provers.

Published
2021

11. General Automation in Coq through Modular Transformations

Author

Valentin Blot, Chantal Keller, Louise Dubois de Prisque, Pierre Vial, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer science, business.industry, Programming language, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Context (language use), Modular design, computer.software_genre, Automation, Logic in Computer Science (cs.LO), Set (abstract data type), Type theory, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Simple (abstract algebra), Proof of concept, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Algebraic data type, business, computer
Abstract

Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further away from first-order logic, the logic of most automatic theorem provers. In this article, we develop a methodology to transform a subset of Coq goals into first-order statements that can be automatically discharged by automatic provers. The general idea is to write modular, pairwise independent transformations and combine them. Each of these eliminates a specific aspect of Coq logic towards first-order logic. As a proof of concept, we apply this methodology to a set of simple but crucial transformations which extend the local context with proven first-order assertions that make Coq definitions and algebraic types explicit. They allow users of Coq to solve non-trivial goals automatically. This methodology paves the way towards the definition and combination of more complex transformations, making Coq more accessible., Comment: In Proceedings PxTP 2021, arXiv:2107.01544

Published
2021
Full Text
View/download PDF

12. The New Rewriting Engine of Dedukti

Author

Hondet, Gabriel, Blanqui, Frédéric, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Centre National de la Recherche Scientifique (CNRS), and Université Paris-Saclay

Subjects
Computer Science - Symbolic Computation, Rewriting algorithm, [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], Computer Science - Programming Languages, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, non-linear higher-order pattern matching
Abstract

International audience; Dedukti is a type-checker for the λΠ-calculus modulo rewriting, an extension of Edinburgh’s logicalframework LF where functions and type symbols can be defined by rewrite rules. It thereforecontains an engine for rewriting LF terms and types according to the rewrite rules given by the user.A key component of this engine is the matching algorithm to find which rules can be fired. In thispaper, we describe the class of rewrite rules supported by Dedukti and the new implementation ofthe matching algorithm. Dedukti supports non-linear rewrite rules on terms with binders usinghigher-order pattern-matching as in Combinatory Reduction Systems (CRS). The new matchingalgorithm extends the technique of decision trees introduced by Luc Maranget in the OCamlcompiler to this more general context.

Published
2020
Full Text
View/download PDF

13. Linking Focusing and Resolution with Selection

Author

Guillaume Burel, Méthodes et modèles pour les réseaux (METHODES-SAMOVAR), Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux (SAMOVAR), Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP)-Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Igor Potapov, Paul Spirakis, and James Worrell

Subjects
General Computer Science, Logic, Computer science, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory, Modulo, 02 engineering and technology, proof theory, Mathematical proof, 01 natural sciences, refinements of resolution, Theoretical Computer Science, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Sequent, 0101 mathematics, automated deduction, 060201 languages & linguistics, polarization, 000 Computer science, knowledge, general works, 010102 general mathematics, Sequent calculus, Atomic formula, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 06 humanities and the arts, 16. Peace & justice, deduction modulo theory, Computational Mathematics, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, sequent calculus, Proof theory, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0602 languages and literature, Computer Science, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.4: Mechanical theorem proving, 020201 artificial intelligence & image processing, Rewriting
Abstract

Focusing and selection are techniques that shrink the proof-search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atomic formula can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory and the related framework called superdeduction; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof-search space.

Published
2020
Full Text
View/download PDF

14. Sharing a Library between Proof Assistants: Reaching out to the HOL Family

Author

François Thiré, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer science, Interoperability, HOL, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, lcsh:QA75.5-76.95, Simple type theory, 0202 electrical engineering, electronic engineering, information engineering, Fermat's Last Theorem, Class (computer programming), Programming language, lcsh:Mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Extension (predicate logic), lcsh:QA1-939, Logic in Computer Science (cs.LO), Theorem provers, Logical framework, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, lcsh:Electronic computers. Computer science, computer
Abstract

We observe today a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to co-operate because they do not implement the same logic. Logical frameworks are a class of theorem provers that overcome this issue by their capacity of implementing various logics. In this work, we study the STTforall logic, an extension of Simple Type Theory that has been encoded in the logical framework Dedukti. We present a translation from this logic to OpenTheory, a proof system and interoperability tool between provers of the HOL family. We have used this translation to export an arithmetic library containing Fermat's little theorem to OpenTheory and to two other proof systems that are Coq and Matita., Comment: In Proceedings LFMTP 2018, arXiv:1807.01352

Published
2018
Full Text
View/download PDF

15. EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)

Author

Mohamed Haddad, Guillaume Burel, Frédéric Blanqui, Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Université Paris-Saclay, ENSIIE, Méthodes et modèles pour les réseaux (METHODES-SAMOVAR), Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux (SAMOVAR), Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP)-Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), and ANR-05-PADD-0011,COPT,Conception d'Observatoires de Pratiques Territorialisées(2005)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Programming language, Computer science, lcsh:Mathematics, HOL, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, Mathematical proof, lcsh:QA1-939, 01 natural sciences, lcsh:QA75.5-76.95, Logic in Computer Science (cs.LO), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Proof calculus, 010201 computation theory & mathematics, Automated proof checking, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0202 electrical engineering, electronic engineering, information engineering, lcsh:Electronic computers. Computer science, computer, TRACE (psycholinguistics)
Abstract

Proof assistants often call automated theorem provers to prove subgoals. However, each prover has its own proof calculus and the proof traces that it produces often lack many details to build a complete proof. Hence these traces are hard to check and reuse in proof assistants. Dedukti is a proof checker whose proofs can be translated to various proof assistants: Coq, HOL, Lean, Matita, PVS. We implemented a tool that extracts TPTP subproblems from a TSTP file and reconstructs complete proofs in Dedukti using automated provers able to generate Dedukti proofs like ZenonModulo or ArchSAT. This tool is generic: it assumes nothing about the proof calculus of the prover producing the trace, and it can use different provers to produce the Dedukti proof. We applied our tool on traces produced by automated theorem provers on the CNF problems of the TPTP library and we were able to reconstruct a proof for a large proportion of them, significantly increasing the number of Dedukti proofs that could be obtained for those problems., In Proceedings PxTP 2019, arXiv:1908.08639

Published
2019
Full Text
View/download PDF

16. Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

Author

Frédéric Blanqui, Guillaume Genestier, Olivier Hermant, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Centre de Recherche en Informatique (CRI), MINES ParisTech - École nationale supérieure des mines de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Marc Bezem, Niels van der Weide, and Mines Paris - PSL (École nationale supérieure des mines de Paris)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Dependent Types, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ComputingMilieux_MISCELLANEOUS, Logic in Computer Science (cs.LO), Dependency Pairs, Termination, Higher-Order Rewriting
Abstract

Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. This extends previous resultsby Wahlstedt on the one hand and the first author on the other hand to strong normalization and non-orthogonal rewriting systems. This new criterion is implemented in the type-checker Dedukti., Comment: FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany

Published
2019
Full Text
View/download PDF

17. Verifiable certificates for predicate subtyping

Author

Gilbert, Frédéric, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), 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)-Laboratoire Spécification et Vérification [Cachan] (LSV), and École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, type theory, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], proof theory, predicate subtyping, higher-order logic
Abstract

Adding predicate subtyping to higher-order logic yields a very expressive language in which type-checking is undecidable, making the definition of a system of verifiable certificates challenging. This work presents a solution to this issue with a minimal formalization of predicate subtyping, named PVS-Core, together with a system of verifiable certificates for PVS-Core, named PVS-Cert. PVS-Cert is based on the introduction of proof terms and explicit coercions. Its design is similar to that of PTSs with dependent pairs, at the exception of the definition of conversion, which is based on a specific notion of reduction → β * , corresponding to β-reduction combined with the erasure of coercions. The use of this reduction instead of the more standard reduction → βσ allows to establish a simple correspondence between PVS-Core and PVS-Cert. On the other hand, a type-checking algorithm is designed for PVS-Cert, built on proofs of type preservation of → βσ and strong normalization of both → βσ and → β *. Using these results, PVS-Cert judgements are used as verifiable certificates for predicate subtyping. In addition, the reduction → βσ is used to define a cut elimination procedure adapted to predicate subtyping. Its use to study the properties of predicate subtyp-ing is illustrated with a proof of consistency.

Published
2019

18. Towards Combining Model Checking and Proof Checking

Author

Kailiang Ji, Jian Liu, Ying Jiang, Gilles Dowek, State Key Laboratory of Computer Science [Beijing] (LCS), Institute of Software Chinese Academy of Sciences [Beijing], Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), Design, study and implementation of languages for proofs and programs (PI.R2), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), and Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)

Subjects
Model checking, Continuation-passing style, Computation tree logic, General Computer Science, Computer science, 0102 computer and information sciences, 02 engineering and technology, Gas meter prover, computer.software_genre, 01 natural sciences, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Automated theorem proving, Temporal logic, Formal verification, Programming language, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Predicate (mathematical logic), Doubly on-the-fly style, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, CTL Model checking, computer, Counterexample
Abstract

International audience; Model checking and automated theorem proving are two pillars of formal verification methods. This paper investigates model checking from an automated theorem proving perspective, aiming at combining the expressiveness of automated theorem proving and the complete automaticity of model checking. It places the focus on the verification of temporal logic properties of Kripke models. The main contributions are: (1) introducing an extended computation tree logic that allows polyadic predicate symbols; (2) designing a proof system for this logic, taking Kripke models as parameters; (3) developing a proof search algorithm for this system and a new automated theorem prover to implement it. The verification process of the new prover is completely automatic, and produces either a counterexample when the property does not hold, or a certificate when it does. The experimental results compare well to existing state-of-the-art tools on some benchmarks, and the efficiency is illustrated by application to an air traffic control problem.

Published
2019
Full Text
View/download PDF

19. Graph Path Orderings

Author

Nachum Dershowitz, Jean-Pierre Jouannaud, School of Computer Science (TAU-CS), Tel Aviv University [Tel Aviv], Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), Gilles Barthe, Geoff Sutcliffe, Margus Veanes, Jouannaud, Jean-Pierre, Tel Aviv University (TAU), and École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Discrete mathematics, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Path-ordering, Computer science, Computation, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Graph, Decidability, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Rewriting, Finite set, MathematicsofComputing_DISCRETEMATHEMATICS
Abstract

International audience; We define well-founded rewrite orderings on graphs and show that they can be used to show termination of a set of graph rewrite rules by verifying all their cyclic extensions. We then introduce the graph path ordering inspired by the recursive path ordering on terms and show that it is a well-founded rewrite ordering on graphs for which checking termination of a finite set of graph rewrite rules is decidable. Our ordering applies to arbitrary finite, directed, labeled, ordered multigraphs, hence provides a building block for rewriting with graphs, which should impact the many areas in which computations take place on graphs.

Published
2018

20. Size-based termination of higher-order rewriting

Author

Frédéric Blanqui, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), and Université Paris-Saclay

Subjects
termination, Computer Science - Logic in Computer Science, subtyping, Computer science, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], 0102 computer and information sciences, Fixed point, Max-plus algebra, 01 natural sciences, size, Operator (computer programming), Bounding overwatch, 0101 mathematics, computer.programming_language, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], 010102 general mathematics, Pareto principle, typing, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Function (mathematics), max-plus algebra, lambda-calculus, rewriting, Algebra, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Rewriting, Lambda calculus, computer, Software
Abstract

We provide a general and modular criterion for the termination of simply typed λ-calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.

Published
2018
Full Text
View/download PDF

21. Unboxing Mutually Recursive Type Definitions in OCaml

Author

Colin, Simon, Lepigre, Rodolphe, Scherer, Gabriel, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), Proof search and reasoning with logic specifications (PARSIFAL), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France, 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)-Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), and É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

Subjects
FOS: Computer and information sciences, Computer Science - Programming Languages, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Programming Languages (cs.PL)
Abstract

In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single field) can sometimes be `unboxed'. This means that their memory representation is the same as their single argument (omitting the variant or record constructor and an indirection), thus achieving better time and memory efficiency. However, in the case of generalized/guarded algebraic datatypes (GADTs), unboxing is not always possible due to a subtle assumption about the runtime representation of OCaml values. The current correctness check is incomplete, rejecting many valid definitions, in particular those involving mutually-recursive datatype declarations. In this paper, we explain the notion of separability as a semantic for the unboxing criterion, and propose a set of inference rules to check separability. From these inference rules, we derive a new implementation of the unboxing check that properly supports mutually-recursive definitions., Comment: accepted at JFLA 2019

Published
2018
Full Text
View/download PDF

22. Exporting an Arithmetic Library from Dedukti to HOL

Author

Thiré, François, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), 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)-Laboratoire Spécification et Vérification [Cachan] (LSV), and École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, OpenTheory, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, HOL, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Interoperability, arithmetic, Dedukti
Abstract

Today, we observe a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to cooperate because they do not implement the same logic. Logical frameworks are a class of theorems provers that overcome this issue by their capacity of implementing various logics. In this work, we study the STT∀ βδ logic, an extension of the Simple Type Theory that has been encoded in the logical framework Dedukti. We show that this new logic is a good candidate to export proofs to other provers. As an example, we show how this logic has been encoded into Dedukti and how we used it to export proofs to the HOL family provers via OpenTheory.

Published
2017

23. Proof certificates in PVS

Author

Frédéric Gilbert, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), Laboratoire Sûreté des Logiciels (LSL), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, Laboratoire d'Intégration des Systèmes et des Technologies (LIST), and Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST)

Subjects
Computer science, Programming language, Proof search, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 02 engineering and technology, Mathematical proof, computer.software_genre, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Fragment (logic), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 020204 information systems, Automated proof checking, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0202 electrical engineering, electronic engineering, information engineering, Instrumentation (computer programming), computer
Abstract

International audience; The purpose of this work is to allow the proof system PVS to export proof certificates that can be checked externally. This is done through the instrumentation of PVS to record detailed proofs step by step during the proof search process. At the current stage of this work, proofs can be built for any PVS theory. However, some reasoning steps rely on unverified assumptions. For a restricted fragment of PVS, the proofs are exported to the universal proof checker Dedukti, and the un-verified assumptions are proved externally using the automated theorem prover MetiTarski.

Published
2017
Full Text
View/download PDF

24. Termination checking in the λΠ-calculus modulo theory.From a practical and a theoretical viewpoint

Author

Genestier, Guillaume, Mines Paris - PSL (École nationale supérieure des mines de Paris), Université Paris sciences et lettres (PSL), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), École normale supérieure - Cachan (ENS Cachan), Université Paris Diderot - Paris 7 (UPD7), Centre de Recherche en Informatique (CRI), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Université Paris Diderot (Paris 7), Olivier Hermant, Frédéric Blanqui, and MINES ParisTech - École nationale supérieure des mines de Paris

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

National audience; Dedukti is a type-checker for the λΠ-calculus modulo theory, which has theparticularity to allow the user to declare rewrite rules, especially in order toencode the logic he/she wants to use. Thanks to the Curry-Howard-De Bruijncorrespondence, the type checking done by Dedukti can be used to check proofs.Unfortunately, to decide the type-checking, Dedukti needs the system ofrewrite rules declared by the user, together with β-reduction, to be confluentand terminating. An external tool already exists to check the confluence, but noautomatic tool exists for the termination, which must be checked independentlyby hand, before using Dedukti.The subject of this report (and more widely of the internship) is to developsuch a tool.A first part of it is dedicated to an algorithm of termination checking: theSize-Change Principle. After a brief introduction to Dedukti, the algorithm isexplained and the results obtained by an implementation of it for Dedukti arepresented.The second and longest part of this report is much more theoretic, sinceit presents reducibility candidates for the λΠ-calculus modulo theory. Thosereducibility candidates can then be used together with the Size-Change Principledetailed in the first part, to check the termination of a rewrite rule system, asexplained in [Wah07].

Published
2017

25. mSAT:An OCaml SAT Solver

Author

Bury, Guillaume, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; mSAT : a SAT solving library in OCaml. It solves the satisfibility of propositional clauses. It is Modular : the user provides the theory. And it produces formal proofs.

Published
2017

26. Models and termination of proof reduction in the λΠ-calculus modulo theory

Author

Dowek, Gilles, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

We define a notion of model for the λΠ-calculus modulo theory and prove a soundness theorem. We then define a notion of super-consistency and prove that proof reduction terminates in the λΠ-calculus modulo any super-consistent theory. We prove this way the termination of proof reduction in several theories including Simple type theory and the Calculus of constructions .

Published
2017

27. The probability of non-confluent systems

Author

Gilles Dowek, Alejandro Díaz-Caro, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and Mauricio Ayala Rincón and Eduardo Bonelli and Ian Mackie

Subjects
FOS: Computer and information sciences, Discrete mathematics, Computer Science - Logic in Computer Science, Lebesgue measure, Computer science, lcsh:Mathematics, Structure (category theory), Probabilistic logic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Type (model theory), Space (mathematics), Lambda, lcsh:QA1-939, lcsh:QA75.5-76.95, Logic in Computer Science (cs.LO), Set (abstract data type), Probability space, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, lcsh:Electronic computers. Computer science
Abstract

We show how to provide a structure of probability space to the set of execution traces on a non-confluent abstract rewrite system, by defining a variant of a Lebesgue measure on the space of traces. Then, we show how to use this probability space to transform a non-deterministic calculus into a probabilistic one. We use as example Lambda+, a recently introduced calculus defined through type isomorphisms., In Proceedings DCM 2013, arXiv:1403.7685

Published
2014
Full Text
View/download PDF

28. Soundly Proving B Method Formulae Using Typed Sequent Calculus

Author

Pierre Halmagrand, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), Augusto Sampaio, Farn Wang, ANR-12-INSE-0010,BWare,Une plate-forme mécanisée et basée sur la preuve pour la vérification d'obligations de preuve B(2012), 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)-Laboratoire Spécification et Vérification [Cachan] (LSV), and École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Discrete mathematics, Natural deduction, Typed Sequent Calculus, Cut-elimination theorem, Proof complexity, 05 social sciences, Sequent calculus, 020207 software engineering, 02 engineering and technology, Curry–Howard correspondence, Proof Translation, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Proof calculus, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, 0502 economics and business, 0202 electrical engineering, electronic engineering, information engineering, Calculus, B Method, 050211 marketing, Sequent, Polymorphic First Order Logic, Mathematics
Abstract

International audience; The B Method is a formal method mainly used in the railway industry to specify and develop safety-critical software. To guarantee the consistency of a B project, one decisive challenge is to show correct a large amount of proof obligations, which are mathematical formulae expressed in a classical set theory extended with a specific type system. To improve automated theorem proving in the B Method, we propose to use a first-order sequent calculus extended with a polymorphic type system, which is in particular the output proof-format of the tableau-based automated theorem prover Zenon. After stating some modifications of the B syntax and defining a sound elimination of comprehension sets, we propose a translation of B formulae into a polymorphic first-order logic format. Then, we introduce the typed sequent calculus used by Zenon, and show that Zenon proofs can be translated to proofs of the initial B formulae in the B proof system.

Published
2016
Full Text
View/download PDF

29. Internship report MPRI 2 Reverse engineering on arithmetic proofs

Author

Thiré, François, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), ENS Cachan, Paris Diderot University, Gilles Dowek, and Stéphane Lengrand

Subjects
MSC, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO]Computer Science [cs]
Abstract

International audience; dedukti is a logical framework that implements the λΠ− modulo theory, an extension of the simply typed lambda calculus with dependent types and rewriting rules. It aims to be a back-end for other proof checkers by compiling proofs from these proof checkers to dedukti. This may also increase re-usability of proofs between proof checkers. However if a logic is more powerful than an other, a theorem in the first logic may not be a theorem in the second. During this internship, we consider arithmetic theorems since many proof checker are able to check arithmetic proofs. One problem that we study in this master thesis is to translate arithmetic proofs coming from a powerful proof checker, -- in our casematita -- to a less powerful proof checker -- HOL-- . This translation needs to modify the logic used in proofs and that is why dedukti is handy here. But a lot of arithmetic theorems are proved also by automatic provers. Indeed, today a lot of easy arithmetic theorems are proved by this kind of tool. But most of them do not give a proof if it claims to prove a theorem. Since for these kind of tool, constructing a full proof may be tiresome, they prefer to give a certificate , a sketch of a proof. However, any automatic prover can implement its own certificate format. To answer this problem, Zakaria Chihani & Dale Miller proposed a certificate framework: Foundational Proof Certificate (FPC) [CMR13]. This framework aims to provide a certificate format shared by many automatic provers so that from the latter, a full proof might be reconstructed.However, for now, no certificate format is given for arithmetic proofs. A second problem addressed in this internship is to answer what kind of certificate is needed for arithmetic proofs (arithmetic without multiplication).

Published
2016

30. Encoding Proofs in Dedukti: the case of Coq proofs

Author

Assaf, Ali, Dowek, Gilles, Jouannaud, Jean-Pierre, Liu, Jiaxiang, Google Inc, Research at Google, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), 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)-Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Tsinghua University [Beijing] (THU), Andrei Voronkov, École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), and École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Logical Frameworks, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Cnfluence, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Calculus of Constructions, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Cumulative Universes, Encodings
Abstract

International audience; A main ambition of the Inria project Dedukti is to serve as a common language for representing and type checking proof objects originating from other proof systems. Encoding these proof objects makes heavy use of the rewriting capabilities of LambdaPiModulo, the formal system on which Dedukti is based. So far, the proofs generated by two automatic proofsystems, Zenon and iProver, have been encoded, and can therefore be read and checked by Dedukti. But Dedukti goes far beyond this so-called hammering technique of sending goals to automated provers. Proofs from HOL and Matita can be encoded as well. Some Coq’s proofs can be encoded already, when they do not use universe polymorphism. Our ambition here is to close this remaining gap. To this end, we describe a rewrite-based encoding in LambdaPiModulo of the Calculus of Constructions with a cumulative hierarchy of predicative universes above Prop, which is confluent on open terms.

Published
2016

31. A Rewrite System for Proof Constructivization

Author

Raphaël Cauderlier, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), 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)-Laboratoire Spécification et Vérification [Cachan] (LSV), and École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Discrete mathematics, 010308 nuclear & particles physics, Proof complexity, 010102 general mathematics, Proof assistant, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Mathematical proof, 01 natural sciences, Computer-assisted proof, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Proof theory, Automated proof checking, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, 0103 physical sciences, Calculus, Structural proof theory, 0101 mathematics, Probabilistically checkable proof, Mathematics
Abstract

International audience; Proof constructivization is the problem of automatically extracting constructive proofs out of classical proofs. This process is required when classical theorem provers are integrated in intuitionistic proof assistants. We use the ability of rewrite systems to represent partial functions to implement heuristics for proof constructivization in Dedukti, a logical framework based on rewriting in which proofs are first-class objects which can be the subject of computation. We benchmark these heuristics on the proofs output by the automated theorem prover Zenon on the TPTP library of problems.

Published
2016
Full Text
View/download PDF

32. Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval

Author

Wang, Shuai, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-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), Gilles Dowek, and Wang, Shuai

Subjects
proof checking, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, higher order logic, [INFO]Computer Science [cs], proofcloud, [INFO] Computer Science [cs]
Abstract

International audience; Higher Order Logic has been used in formal mathematics, software verification and hardware verification over the past decades. Recent developments of interactive theorem made sharing proofs between some theorem provers possible. This paper first gives an introduction and an overview of related recent advances, followed by the proof checking benchmarks of a proof sharing repository, namely OpenTheory (after proof transformation by the upgraded Holide). Finally, we introduce ProofCloud, the first proof retrieval engine for higher order proofs.

Published
2016

33. Termination of rewrite relations on λ-terms based on Girard's notion of reducibility

Author

Frédéric Blanqui, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
termination, Computer Science - Logic in Computer Science, General Computer Science, Matching (graph theory), ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.3: Studies of Program Constructs/F.3.3.3: Program and recursion schemes, Modulo, rewriting modulo, 0102 computer and information sciences, 02 engineering and technology, ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.2: Semantics of Programming Languages/F.3.2.2: Operational semantics, 01 natural sciences, Theoretical Computer Science, matching modulo βη, Simple (abstract algebra), Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Girard's reducibility, 0202 electrical engineering, electronic engineering, information engineering, patterns a la Miller, types, Equational theory, ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs/F.3.1.3: Mechanical verification, Mathematics, Computability, λ-calculus, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Mathematics - Logic, rewriting, Algebra, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.2: Lambda calculus and related systems, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Closure (mathematics), 010201 computation theory & mathematics, Confluence, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Rewriting
Abstract

In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of $\beta$-reduction in the polymorphic $\lambda$-calculus, to prove the termination of various kinds of rewrite relations on $\lambda$-terms, including rewriting modulo some equational theory and rewriting with matching modulo $\beta$$\eta$, by using the notion of computability closure. This provides a powerful termination criterion for various higher-order rewriting frameworks, including Klop's Combinatory Reductions Systems with simple types and Nipkow's Higher-order Rewrite Systems.

Published
2015
Full Text
View/download PDF

34. Normalization by Completeness with Heyting Algebras

Author

Gaëtan Gilbert, Olivier Hermant, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École normale supérieure - Lyon (ENS Lyon), Department of Mathematics and Computer Science, Wesleyan University, MINES ParisTech - École nationale supérieure des mines de Paris, Université Paris sciences et lettres (PSL), Centre de Recherche en Informatique (CRI), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), École normale supérieure de Lyon (ENS de Lyon), and Mines Paris - PSL (École nationale supérieure des mines de Paris)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; Usual normalization by evaluation techniques have a strong relationship with completeness with respect to Kripke structures. But Kripke structures is not the only semantics that ts intuitionistic logic: Heyting algebras are a more algebraic alternative.In this paper, we focus on this less investigated area: how completeness with respect to Heyting algebras generate a normalization algorithm for a natural deduction calculus, in the propositional fragment. Our main contributions is that we prove in a direct way completeness of natural deduction with respect to Heyting algebras, that the underlying algorithm natively deals with disjunction, that we formalized those proofs in Coq, and give an extracted algorithm.

Published
2015

35. Implementing Polymorphism in Zenon

Author

Bury, Guillaume, Cauderlier, Raphaël, Halmagrand, Pierre, Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre d'enseignement Cnam Paris (CNAM Paris), Conservatoire National des Arts et Métiers [CNAM] (CNAM), and ANR-12-INSE-0010,BWare,Une plate-forme mécanisée et basée sur la preuve pour la vérification d'obligations de preuve B(2012)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Abstract

Extending first-order logic with ML-style polymorphism allows to definegeneric axioms dealing with several sorts. Until recently, mostautomated theorem provers relied on preprocess encodings intomono/many-sorted logic to reason within such theories. In this paper, wediscuss the implementation of polymorphism into thefirst-order tableau-based automated theorem prover Zenon. Thisimplementation leads to slightly modify some basic parts of the code,from the representation of expressions to the proof-search algorithm.

Published
2015

36. Translating HOL to Dedukti

Author

Guillaume Burel, Ali Assaf, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École polytechnique (X), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Cezary Kaliszyk, and Andrei Paskevich

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer science, Modulo, HOL, Higher Order Logic, Mathematical proof, computer.software_genre, Translation (geometry), Higher-order logic, lcsh:QA75.5-76.95, Reduction (complexity), Computer Science::Logic in Computer Science, [INFO]Computer Science [cs], logical embedding, dependent types, Programming language, lcsh:Mathematics, lcsh:QA1-939, Logic in Computer Science (cs.LO), rewriting, Logical framework, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, logical framework, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, dedukti, F.4.1, lcsh:Electronic computers. Computer science, Rewriting, computer
Abstract

Dedukti is a logical framework based on the lambda-Pi-calculus modulo rewriting, which extends the lambda-Pi-calculus with rewrite rules. In this paper, we show how to translate the proofs of a family of HOL proof assistants to Dedukti. The translation preserves binding, typing, and reduction. We implemented this translation in an automated tool and used it to successfully translate the OpenTheory standard library., In Proceedings PxTP 2015, arXiv:1507.08375

Published
2015
Full Text
View/download PDF

37. Rewriting Modulo β in the λ Π-Calculus Modulo

Author

Ronan Saillard, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre de Recherche en Informatique (CRI), MINES ParisTech - École nationale supérieure des mines de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), and Mines Paris - PSL (École nationale supérieure des mines de Paris)

Subjects
Discrete mathematics, Modulo, lcsh:Mathematics, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, Type (model theory), lcsh:QA1-939, 01 natural sciences, lcsh:QA75.5-76.95, Logical framework, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Confluence, Encoding (memory), Computer Science::Logic in Computer Science, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Subject reduction, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Computer Science::Programming Languages, Uniqueness, Rewriting, lcsh:Electronic computers. Computer science, 0101 mathematics, Mathematics
Abstract

The lambda-Pi-calculus Modulo is a variant of the lambda-calculus with dependent types where beta-conversion is extended with user-defined rewrite rules. It is an expressive logical framework and has been used to encode logics and type systems in a shallow way. Basic properties such as subject reduction or uniqueness of types do not hold in general in the lambda-Pi-calculus Modulo. However, they hold if the rewrite system generated by the rewrite rules together with beta-reduction is confluent. But this is too restrictive. To handle the case where non confluence comes from the interference between the beta-reduction and rewrite rules with lambda-abstraction on their left-hand side, we introduce a notion of rewriting modulo beta for the lambda-Pi-calculus Modulo. We prove that confluence of rewriting modulo beta is enough to ensure subject reduction and uniqueness of types. We achieve our goal by encoding the lambda-Pi-calculus Modulo into Higher-Order Rewrite System (HRS). As a consequence, we also make the confluence results for HRSs available for the lambda-Pi-calculus Modulo.

Published
2015
Full Text
View/download PDF

38. Checking Zenon Modulo Proofs in Dedukti

Author

Raphaël Cauderlier, Pierre Halmagrand, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre d'enseignement Cnam Paris (CNAM Paris), Conservatoire National des Arts et Métiers [CNAM] (CNAM), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), ANR-12-INSE-0010,BWare,Une plate-forme mécanisée et basée sur la preuve pour la vérification d'obligations de preuve B(2012), and HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer science, lcsh:Mathematics, Modulo, Extension (predicate logic), lcsh:QA1-939, Mathematical proof, lcsh:QA75.5-76.95, Logic in Computer Science (cs.LO), Proof Checking, Logical framework, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Automated proof checking, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Calculus, Embedding, lcsh:Electronic computers. Computer science, Rewriting
Abstract

Dedukti has been proposed as a universal proof checker. It is a logical framework based on the lambda Pi calculus modulo that is used as a backend to verify proofs coming from theorem provers, especially those implementing some form of rewriting. We present a shallow embedding into Dedukti of proofs produced by Zenon Modulo, an extension of the tableau-based first-order theorem prover Zenon to deduction modulo and typing. Zenon Modulo is applied to the verification of programs in both academic and industrial projects. The purpose of our embedding is to increase the confidence in automatically generated proofs by separating untrusted proof search from trusted proof verification., In Proceedings PxTP 2015, arXiv:1507.08375

Published
2015

39. Objects and subtyping in the λΠ-calculus modulo

Author

Cauderlier, Raphaël, Dubois, Catherine, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre d'enseignement Cnam Paris (CNAM Paris), Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), and Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Computer Science::Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

We present a shallow embedding of the Object Calculus of Abadi and Cardelli in the λΠ-calculus modulo, an extension of the λΠ-calculus in which conversion is considered modulo a rewrite system. This embedding may be used as an example of translation of subtyping, a feature also present in some proof assistants like Coq and PVS. This embedding is proved correct with respect to the operational semantics and the type system of the Object Calculus. It has been implemented as a translation tool from the Object Calculus to Dedukti, a type-checker for the λΠ-calculus modulo.

Published
2015

40. Conservativity of embeddings in the lambda Pi calculus modulo rewriting (long version)

Author

Assaf, Ali, École polytechnique (X), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], pure type systems, Logic in Computer Science (cs.LO), normalization, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, logical framework, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, [INFO]Computer Science [cs], λΠ calculus modulo rewriting, conservativity
Abstract

The lambda Pi calculus can be extended with rewrite rules to embed any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda Pi calculus modulo rewriting as a logical framework for logics based on pure type systems. This result was previously only proved under the condition that the target system is normalizing. Our approach does not depend on this condition and therefore also works when the source system is not normalizing., Long version of TLCA 2015 paper

Published
2015

41. A Calculus of Constructions with Explicit Subtyping

Author

Assaf, Ali, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École polytechnique (X), Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau

Subjects
000 Computer science, knowledge, general works, subtyping, cumulativity, explicit coercions, 0102 computer and information sciences, 02 engineering and technology, 16. Peace & justice, 01 natural sciences, universes, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, type theory, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Computer Science::Programming Languages, [INFO]Computer Science [cs], 020201 artificial intelligence & image processing, Software_PROGRAMMINGLANGUAGES, calculus of constructions
Abstract

International audience; The calculus of constructions can be extended with an infinite hierarchy of universes and cumulative subtyping. In this hierarchy, each universe is contained in a higher universe. Subtyping is usually left implicit in the typing rules. We present an alternative version of the calculus of constructions where subtyping is explicit. This new system avoids problems related to coercions and dependent types by using the Tarski style of universes and by introducing additional equations to reflect equality.

Published
2015
Full Text
View/download PDF

42. Mixing HOL and Coq in Dedukti (Rough Diamond)

Author

Assaf, Ali, Cauderlier, Raphaël, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École polytechnique (X), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), and HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO]Computer Science [cs]
Abstract

We use Dedukti as a logical framework for interoperability. We use automated tools to translate different developments made in HOL and in Coq to Dedukti and we combine them to prove new results.

Published
2015

43. CTL Model Checking in Deduction Modulo

Author

Kailiang Ji, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
Predicate logic, Model checking, Logical equivalence, Mathematics::Number Theory, Modulo, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Resolution (logic), Model Checking, Algebra, CTL, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Encoding (memory), ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Deduction Modulo, Resolution Modulo, Focus (optics), Mathematics
Abstract

International audience; In this paper we give an overview of proof-search method for CTL model checking based on Deduction Modulo. Deduction Modulo is a reformulation of Predicate Logic where some axioms—possibly all—are replaced by rewrite rules. The focus of this paper is to give an encoding of temporal properties expressed in CTL, by translating the logical equivalence between temporal operators into rewrite rules. This way, the proof-search algorithms designed for Deduction Modulo, such as Resolution Modulo or Tableaux Modulo, can be used in verifying temporal properties of finite transition systems. An experimental evaluation using Resolution Modulo is presented.

Published
2015
Full Text
View/download PDF

44. Call-by-value, call-by-name and the vectorial behaviour of the algebraic \lambda-calculus

Author

Simon Perdrix, Alejandro Díaz-Caro, Benoît Valiron, Christine Tasson, Ali Assaf, École polytechnique (X), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Universidad Nacional de Quilmes (UNQ), Theoretical adverse computations, and safety (CARTE), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), and ANR-10-BLAN-0213,LOGOI,Logique et géometrie de l'interaction(2010)

Subjects
Computer Science - Logic in Computer Science, ACM: F.: Theory of Computation/F.1: COMPUTATION BY ABSTRACT DEVICES/F.1.1: Models of Computation, General Computer Science, Structure (category theory), [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Theoretical Computer Science, Set (abstract data type), linear-algebraic lambda-calculus, Fragment (logic), CPS simulation, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Calculus, Algebraic lambda-calculus, Algebraic number, Linear combination, Mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 16. Peace & justice, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.2: Lambda calculus and related systems, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Confluence, Computer Science::Programming Languages, Rewriting, Differential (mathematics)
Abstract

International audience; We examine the relationship between the algebraic lambda-calculus, a fragment of the differential lambda-calculus and the linear-algebraic lambda-calculus, a candidate lambda-calculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalar-multiplicative structure, and their set of terms is closed under linear combinations. However, the two languages were built using different approaches: the former is a call-by-name language whereas the latter is call-by-value; the former considers algebraic equalities whereas the latter approaches them through rewrite rules. In this paper, we analyse how these different approaches relate to one another. To this end, we propose four canonical languages based on each of the possible choices: call-by-name versus call-by-value, algebraic equality versus algebraic rewriting. We show that the various languages simulate one another. Due to subtle interaction between beta-reduction and algebraic rewriting, to make the languages consistent some additional hypotheses such as confluence or normalisation might be required. We carefully devise the required properties for each proof, making them general enough to be valid for any sub-language satisfying the corresponding properties.

Published
2014
Full Text
View/download PDF

45. Cut Admissibility by Saturation

Author

Guillaume Burel, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and Gilles Dowek

Subjects
Discrete mathematics, deduction modulo, Natural deduction, Modulo, superposition, Sequent calculus, resolution, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Resolution (logic), Term (logic), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, sequent calculus, Confluence, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Calculus, Rewriting, Rule of inference, completion, conditional rewriting, Mathematics
Abstract

International audience; Deduction modulo is a framework in which theories are integrated intoproof systems such as natural deduction or sequent calculus bypresenting them using rewriting rules. When only terms are rewritten,cut admissibility in those systems is equivalent to the confluence ofthe rewriting system, as shown by Dowek, RTA 2003, LNCS 2706. This isno longer true when considering rewriting rules involvingpropositions. In this paper, we show that, in the same way that it ispossible to recover confluence using Knuth-Bendix completion, one canregain cut admissibility in the general case using standardsaturation techniques. This work relies on a view of propositionrewriting rules as oriented clauses, like term rewriting rules can beseen as oriented equations. This also leads us to introduce anextension of deduction modulo with *conditional* term rewritingrules.

Published
2014
Full Text
View/download PDF

46. Using Deduction Modulo in Set Theory

Author

Halmagrand, Pierre, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), ANR-12-INSE-0010,BWare,Une plate-forme mécanisée et basée sur la preuve pour la vérification d'obligations de preuve B(2012), and HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)

Subjects
Rewriting, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Deduction Mod-ulo, Tableaux, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Set Theory, Zenon Modulo, B Method, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Automated Theorem Proving
Abstract

International audience; We present some improvements of Zenon Modulo and the application of this tool to sets of problems coming from set theory. Zenon Modulo is an extension of the tableau-based first order automated theorem prover Zenon to deduction modulo. Deduction modulo is an ex-tension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well-suited for proof-search in axiomatic theories, as it turns axioms into rewrite rules. The improvements dis-cussed here consist in a better heuristic to automatically build rewrite systems given a set of axioms, and some optimizations in the rewrit-ing process used during the proof search. We also present some updated results obtained on benchmarks provided by the TPTP library for set theory categories. Finally, we discuss some recent work about the appli-cation of our tool to the B method set theory, in particular the way we treat equality and the comprehension scheme.

Published
2014

47. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo

Author

Pierre Halmagrand, David Delahaye, Frédéric Gilbert, Olivier Hermant, Damien Doligez, Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), Programming languages, types, compilation and proofs (GALLIUM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Centre de Recherche en Informatique (CRI), Mines Paris - PSL (École nationale supérieure des mines de Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Ken McMillan and Aart Middeldorp and Andrei Voronkov, and MINES ParisTech - École nationale supérieure des mines de Paris

Subjects
Rewriting, Computer science, Modulo, 02 engineering and technology, Dedukti, Proof Checking, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Automated proof checking, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Deduction Modulo, Set theory, Axiom, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], 020207 software engineering, Extension (predicate logic), Zenon, First-order logic, Automated theorem proving, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Tableaux, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 020201 artificial intelligence & image processing, Algorithm, Automated The- orem Proving
Abstract

International audience; We propose an extension of the tableau-based first order automated theorem prover Zenon to deduction modulo. The theory of deduction modulo is an extension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. We also present a heuristic to perform this latter step automatically, and assess our approach by providing some experimental results obtained on the benchmarks provided by the TPTP library, where this heuristic is able to prove difficult problems in set theory in particular. Finally, we describe an additional backend for Zenon that outputs proof certificates for Dedukti, which is a proof checker based on the λΠ-calculus modulo.

Published
2013
Full Text
View/download PDF

48. Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps

Author

David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), Programming languages, types, compilation and proofs (GALLIUM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Centre de Recherche en Informatique (CRI), MINES ParisTech - École nationale supérieure des mines de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Stephan Schulz and Geoff Sutcliffe and Boris Konev, HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), and Mines Paris - PSL (École nationale supérieure des mines de Paris)

Subjects
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.4: Mechanical theorem proving, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]
Abstract

International audience; We present the certifying part of the Zenon Modulo automated theorem prover, which is an extension of the Zenon tableau-based first order automated theorem prover to deduction modulo. The theory of deduction modulo is an extension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. In addition, deduction modulo allows Zenon Modulo to compress proofs by making computations implicit in proofs. To certify these proofs, we use Dedukti, an external proof checker for the λΠ-calculus modulo, which can deal natively with proofs in deduction modulo. To assess our approach, we rely on some experimental results obtained on the benchmarks provided by the TPTP library.

Published
2013

49. Towards explicit rewrite rules in the λΠ-calculus modulo

Author

Saillard, Ronan, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre de Recherche en Informatique (CRI), MINES ParisTech - École nationale supérieure des mines de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), and Mines Paris - PSL (École nationale supérieure des mines de Paris)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Computer Science::Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; This paper provides a new presentation of the λΠ-calculus modulo where the addition of rewrite rules is made explicit. The λΠ-calculus modulo is a variant of the λ-calculus with dependent types where β-reduction is extended with user-defined rewrite rules. Its expressiveness makes it suitable to serve as an output language for theorem provers, certified development tools or proof assistants. Addition of rewrite rules becomes an iterative process and rules previously added can be used to type new rules. We also discuss the condition rewrite rules must satisfy in order to preserve the Subject Reduction property and we give a criterion weaker than the usual one. Finally we describe the new version of Dedukti, a type-checker for the λΠ-calculus modulo for which we assess its efficiency in comparison with Coq, Twelf and Maude.

Published
2013

50. A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo

Author

Burel, Guillaume, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), and Jasmin Christian Blanchette and Josef Urban

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; The λΠ-calculus modulo is a proof language that has been proposed as a proof standard for (re-)checking and interoperability. Resolution and superposition are proof-search methods that are used in state-of-the-art first-order automated theorem provers. We provide a shallow embedding of resolution and superposition proofs in the λΠ-calculus modulo, thus offering a way to check these proofs in a trusted setting, and to combine them with other proofs. We implement this embedding as a back-end of the prover iProver Modulo.

Published
2013

Catalog

Books, media, physical & digital resources
See catalog results