A general method for using schematizations in automated deduction

DOI10.1007/3-540-45744-5_48MaRDI QIDQ4539642zbMATH OpenFDO

Authors Nicolas Peltier

Publication date 10 July 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2083/20830578

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 6938205
• A survey of automated deduction
• Schema induction for logic program synthesis
• scientific article; zbMATH DE number 3972241
• A new application for explanation-based generalisation within automated deduction
• Automated deduction by theory resolution
• scientific article; zbMATH DE number 1552519
• Abstract interpretation as automated deduction

Cited in

(6)

• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• Proofs as schemas and their heuristic use
• The first order theory of primal grammars is decidable
• A complete superposition calculus for primal grammars
• scientific article; zbMATH DE number 6938205 (Why is no real title available?)
• Analogy in automated deduction: a survey

This page was built for publication: A general method for using schematizations in automated deduction

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