scientific article; zbMATH DE number 3956408

MaRDI QIDQ3725520zbMATH OpenFDO

Authors Tadashi Kanamori, Hirohisa Seki

Publication date 1986

zbMATH Keywords

Boyer and Moore theorem provernatural deductionprogram verificationProlog interpreterProlog programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 4074450
• scientific article; zbMATH DE number 868104
• Verification of logic programs
• Reasoning about termination of pure Prolog programs
• Proof methods of declarative properties of definite programs

Cited in

(15)

• Automatic inductive theorem proving using Prolog
• An operational formal definition of PROLOG: A specification method and its application
• Logic program synthesis from incomplete specifications
• Appropriate lemmae discovery
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• scientific article; zbMATH DE number 1615261 (Why is no real title available?)
• scientific article; zbMATH DE number 4157865 (Why is no real title available?)
• scientific article; zbMATH DE number 3965464 (Why is no real title available?)
• scientific article; zbMATH DE number 4047053 (Why is no real title available?)
• scientific article; zbMATH DE number 4074450 (Why is no real title available?)
• A verified prolog compiler for the Warren Abstract Machine
• scientific article; zbMATH DE number 1540615 (Why is no real title available?)
• scientific article; zbMATH DE number 868104 (Why is no real title available?)
• Towards Verifying Logic Programs in the Input Language of clingo
• Design verification of digital systems based on logic programming

This page was built for publication:

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