Proof checking and logic programming

DOI10.1007/S00165-016-0393-ZMaRDI QIDQ2628296zbMATH OpenOpenAlexWikidataFDO

Authors Yanyan Li

Publication date 1 June 2017

Published in Formal Aspects of Computing (Search for Journal in Brave)

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

zbMATH Keywords

logic programmingfocused proof systemsproof checkingproof certificates

Mathematics Subject Classification ID

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

Recommendations

• Proof checking and logic programming
• scientific article; zbMATH DE number 3880145
• scientific article; zbMATH DE number 868104
• Verification of logic programs
• Proving and programming
• scientific article; zbMATH DE number 4195154
• scientific article; zbMATH DE number 4006266
• scientific article; zbMATH DE number 4120164
• scientific article; zbMATH DE number 3907752
• Logic and proof-search procedures

Cites work

• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 6863660 (Why is no real title available?)
• scientific article; zbMATH DE number 786494 (Why is no real title available?)
• scientific article; zbMATH DE number 6741937 (Why is no real title available?)
• A SAT attack on the Erdős discrepancy conjecture
• 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 proof theory for generic judgments
• A proposal for broad spectrum proof certificates
• A semantic framework for proof evidence
• A two-level logic approach to reasoning about computations
• Abella: a system for reasoning about relational specifications
• Call-by-Value  -calculus and LJQ
• Cut-elimination for a logic with definitions and induction
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• ELPI: fast, embeddable, \(\lambda \)Prolog interpreter
• Edinburgh LCF. A mechanized logic of computation
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Focused labeled proof systems for modal logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Foundational proof certificates in first-order logic
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Oracle-based checking of untrusted software
• Programming with higher-order logic.
• Proof certificates for equality reasoning
• The Four Colour Theorem: Engineering of a Formal Proof
• The Proof Certifier Checkers
• Uniform proofs as a foundation for logic programming

Cited in

(6)

• The occur-check problem in Prolog
• Functions-as-constructors higher-order unification: extended pattern unification
• Proof checking and logic programming
• Batch ZK Proof and Verification of OR Logic
• Machine Checking Proof Theory: An Application of Logic to Logic
• A Survey of the Proof-Theoretic Foundations of Logic Programming

Describes a project that uses

Uses Software

• ELPI
• kepler98
• Teyjus
• seL4
• dedukti
• DRAT-trim
• Abella
• Bedwyr
• LCF
• Twelf
• ML

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 Q2628296)