Proof checking and logic programming

DOI10.1007/s00165-016-0393-zzbMath1362.68056OpenAlexW2511942492MaRDI QIDQ2628296

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 in computer science (03B70) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Functions-as-constructors higher-order unification: extended pattern unification, A Survey of the Proof-Theoretic Foundations of Logic Programming

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• A logical characterization of forward and backward chaining in the inverse method
• Focusing and polarization in linear, intuitionistic, and classical logics
• Cut-elimination for a logic with definitions and induction
• A semantic framework for proof evidence
• Proof certificates for equality reasoning
• Edinburgh LCF. A mechanized logic of computation
• A two-level logic approach to reasoning about computations
• A proof of the Kepler conjecture
• Uniform proofs as a foundation for logic programming
• Programming with Higher-Order Logic
• A Proposal for Broad Spectrum Proof Certificates
• A SAT Attack on the Erdős Discrepancy Conjecture
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• The Proof Certifier Checkers
• Focused Labeled Proof Systems for Modal Logic
• ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
• The Four Colour Theorem: Engineering of a Formal Proof
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A new constructive logic: classic logic
• Logic Programming with Focusing Proofs in Linear Logic
• A framework for defining logics
• Foundational Proof Certificates in First-Order Logic
• Oracle-based checking of untrusted software
• Abella: A System for Reasoning about Relational Specifications
• A proof theory for generic judgments
• Call-by-Value  -calculus and LJQ
• Least and Greatest Fixed Points in Linear Logic