Proof Checking and Logic Programming

DOI10.1007/978-3-319-27436-2_1zbMath1362.68055OpenAlexW2400995082MaRDI QIDQ5743582

No author found.

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)

Related Items

A semantic framework for proof evidence, Scalable fine-grained proofs for formula processing

Uses Software

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

Cites Work

• Linear logic
• A logical characterization of forward and backward chaining in the inverse method
• Focusing and polarization in linear, intuitionistic, and classical logics
• 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
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• 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
• Call-by-Value  -calculus and LJQ
• A formulation of the simple theory of types
• Unnamed Item
• Unnamed Item