Proof checking and logic programming
From MaRDI portal
Publication:2628296
DOI10.1007/S00165-016-0393-ZzbMATH Open1362.68056OpenAlexW2511942492WikidataQ130849065 ScholiaQ130849065MaRDI QIDQ2628296FDOQ2628296
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
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
Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cites Work
- Edinburgh LCF. A mechanized logic of computation
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Abella: a system for reasoning about relational specifications
- A proof of the Kepler conjecture
- ELPI: fast, embeddable, \(\lambda \)Prolog interpreter
- Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
- Title not available (Why is that?)
- A framework for defining logics
- Linear logic
- A two-level logic approach to reasoning about computations
- Programming with higher-order logic.
- Focusing and polarization in linear, intuitionistic, and classical logics
- A new constructive logic: classic logic
- Logic Programming with Focusing Proofs in Linear Logic
- Uniform proofs as a foundation for logic programming
- Cut-elimination for a logic with definitions and induction
- Title not available (Why is that?)
- The Four Colour Theorem: Engineering of a Formal Proof
- A SAT attack on the Erdős discrepancy conjecture
- Title not available (Why is that?)
- A proof theory for generic judgments
- Call-by-Value -calculus and LJQ
- A logical characterization of forward and backward chaining in the inverse method
- Oracle-based checking of untrusted software
- Title not available (Why is that?)
- A semantic framework for proof evidence
- Proof certificates for equality reasoning
- The Proof Certifier Checkers
- Focused labeled proof systems for modal logic
- Foundational proof certificates in first-order logic
- Title not available (Why is that?)
- A proposal for broad spectrum proof certificates
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
Uses Software
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)
