Levationis Laus

DOI10.1093/LOGCOM/3.5.487MaRDI QIDQ4286221zbMATH OpenOpenAlexFDO

Authors Kees Doets

Publication date 27 April 1994

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/3.5.487

zbMATH Keywords

inferencecompletenessliftingsheavesunificationterminationSLD-resolutiongreatest fixed-points

Mathematics Subject Classification ID

Logic programming (68N17) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 3872640
• On the completeness of SLDENF-resolution
• A direct proof of the completeness of SLDNF-resolution
• A completeness theorem for SLDNF resolution
• A note on SLDNF-resolution

Cited in

(6)

• A framework for computing finite SLD trees
• Leaping shampoo
• A full formalization of SLD-resolution in the calculus of inductive constructions
• Vervaat et Lévy
• scientific article; zbMATH DE number 219937 (Why is no real title available?)
• Soundness and completeness versus lifting property

This page was built for publication: Levationis Laus

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