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

DOI10.1023/A:1006242018697zbMATH Open0943.68110MaRDI QIDQ1961920FDOQ1961920

Authors: M. Jaume 

Publication date: 5 September 2000

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

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

zbMATH Keywords

semantics of definite programs

Mathematics Subject Classification ID

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

Cited In (3)

• SLT-resolution for the well-founded semantics
• Generalising unit-refutation completeness and SLUR via nested input resolution
• Title not available (Why is that?)

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)