Foundational Proof Certificates in First-Order Logic
| Autor: | Fabien Renaud, Dale Miller, Zakaria Chihani |
|---|---|
| Přispěvatelé: | Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), 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, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Renaud, Fabien, É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 |
| Rok vydání: | 2013 |
| Předmět: |
Discrete mathematics
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] Proof complexity Proof Proof by contradiction 010102 general mathematics Proof assistant [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 0102 computer and information sciences Mathematical proof 01 natural sciences TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Proof theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Calculus Structural proof theory 0101 mathematics Mathematics Analytic proof |
| Zdroj: | Automated Deduction – CADE-24 ISBN: 9783642385735 CADE CADE-24th International Conference on Automated Deduction CADE-24th International Conference on Automated Deduction, Jun 2013, Lake Placid, United States Lecture Notes in Computer Science |
| Popis: | International audience; It is the exception that provers share and trust each others proofs. One reason for this is that different provers structure their proof evidence in remarkably different ways, including, for example, proof scripts, resolution refutations, tableaux, Herbrand expansions, natural deductions, etc. In this paper, we propose an approach to foundational proof certificates as a means of flexibly presenting proof evidence so that a relatively simple and universal proof checker can check that a certificate does, indeed, elaborate to a formal proof. While we shall limit ourselves to first-order logic in this paper, we shall not limit ourselves in many other ways. Our framework for defining and checking proof certificates will work with classical and intuitionistic logics and with proof structures as diverse as resolution refutations, matings, and natural deduction. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|