A full formalization of SLD-resolution in the calculus of inductive constructions

DOI10.1023/A:1006242018697MaRDI QIDQ1961920zbMATH OpenFDO

Authors M. Jaume

Publication date 5 September 2000

Published in Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

semantics of definite programs

Mathematics Subject Classification ID

Logic programming (68N17) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 1059317
• Formalization of the resolution calculus for first-order logic
• Formalization of the Resolution Calculus for First-Order Logic
• Levationis Laus
• A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules

Cited in

(5)

• Generalising unit-refutation completeness and SLUR via nested input resolution
• Certified semantics for relational programming
• SLT-resolution for the well-founded semantics
• scientific article; zbMATH DE number 683357 (Why is no real title available?)
• Formalization of the resolution calculus for first-order logic

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A full formalization of SLD-resolution in the calculus of inductive constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1961920)