Proof checking and logic programming

DOI10.1007/978-3-319-27436-2_1MaRDI QIDQ5743582zbMATH OpenOpenAlexFDO

Authors

Publication date 5 February 2016

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01390901/file/paper.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Proof checking and logic programming
• A trustworthy proof checker
• Foundational proof certificates in first-order logic
• scientific article; zbMATH DE number 4172362
• The Proof Certifier Checkers

Cites work

• A formulation of the simple theory of types
• A framework for defining logics
• A logical characterization of forward and backward chaining in the inverse method
• A new constructive logic: classic logic
• A proof of the Kepler conjecture
• A two-level logic approach to reasoning about computations
• Call-by-Value  -calculus and LJQ
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Edinburgh LCF. A mechanized logic of computation
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Focusing and polarization in linear, intuitionistic, and classical logics
• Foundational proof certificates in first-order logic
• scientific article; zbMATH DE number 786494 (Why is no real title available?)
• scientific article; zbMATH DE number 6741937 (Why is no real title available?)
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Programming with higher-order logic.
• The Four Colour Theorem: Engineering of a Formal Proof
• Uniform proofs as a foundation for logic programming

Cited in

(7)

• The occur-check problem in Prolog
• A semantic framework for proof evidence
• Proof checking and logic programming
• Machine Checking Proof Theory: An Application of Logic to Logic
• Batch ZK Proof and Verification of OR Logic
• scientific article; zbMATH DE number 813263 (Why is no real title available?)
• Scalable fine-grained proofs for formula processing

Describes a project that uses

Uses Software

• ML
• Twelf
• kepler98
• Abella
• DRAT-trim
• dedukti
• seL4
• Teyjus

This page was built for publication: Proof checking and logic programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5743582)