A Semantic Framework for Proof Evidence
Autor: | Dale Miller, Zakaria Chihani, Fabien Renaud |
---|---|
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), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), É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, École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS) |
Jazyk: | angličtina |
Rok vydání: | 2017 |
Předmět: |
0102 computer and information sciences
computer.software_genre Mathematical proof 01 natural sciences Formal proof Computer-assisted proof Artificial Intelligence Computer Science::Logic in Computer Science Structural proof theory 0101 mathematics Mathematics focused proof systems Discrete mathematics Proof complexity Programming language 010102 general mathematics Proof assistant [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] proof checking TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics 010201 computation theory & mathematics Proof theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS computer Software foundational proof certificates Analytic proof |
Zdroj: | Journal of Automated Reasoning Journal of Automated Reasoning, Springer Verlag, 2017, 59 (3), pp.287-330. ⟨10.1007/s10817-016-9380-6⟩ Journal of Automated Reasoning, 2017, 59 (3), pp.287-330. ⟨10.1007/s10817-016-9380-6⟩ |
ISSN: | 0168-7433 1573-0670 |
Popis: | International audience; Theorem provers produce evidence of proof in many different formats, such as proof scripts, natural deductions, resolution refutations, Herbrand expansions, and equational rewritings. In implemented provers, numerous variants of such formats are actually used: consider, for example, such variants of or restrictions to resolution refu-tations as binary resolution, hyper-resolution, ordered-resolution, paramodulation, etc. We propose the foundational proof certificates (FPC) framework for defining the semantics of a broad range of proof evidence. This framework allows both producers of proof certificates and the checkers of those certificates to have a clear formal definition of the semantics of a wide variety of proof evidence. Employing the FPC framework will allow one to separate a proof from its provenance and to allow anyone to construct their own proof checker for a given style of proof evidence. The foundation on which FPC relies is that of proof theory, particularly recent work into focused proof systems: such proof systems provide protocols by which a checker extracts information from the certificate (mediated by the so called clerks and experts) as well as performs various deterministic and non-deterministic computations. While we shall limit ourselves to first-order logic in this paper, we shall not limit ourselves in many other ways. The FPC framework is described for both classical and intuitionistic logics and for proof structures as diverse as resolution refutations, natural deduction, Frege proofs, and equality proofs. |
Databáze: | OpenAIRE |
Externí odkaz: |