Proof checking and logic programming
From MaRDI portal
Publication:2628296
DOI10.1007/s00165-016-0393-zzbMath1362.68056OpenAlexW2511942492MaRDI QIDQ2628296
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
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
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
