Little engines of proof

DOI10.1007/3-540-45614-7_1MaRDI QIDQ4808819zbMATH OpenFDO

Authors Natarajan Shankar

Publication date 12 August 2004

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/2391/23910001.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Deciding Combinations of Theories
• Mechanizing Mathematical Reasoning
• Formal verification of a combination decision procedure
• Combining decision procedures.
• Strategies for combining decision procedures

Cited in

(11)

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• From LCF to Isabelle/HOL
• Strategies for combining decision procedures
• Canonization for disjoint unions of theories
• Semantically-guided goal-sensitive reasoning: model representation
• scientific article; zbMATH DE number 140415 (Why is no real title available?)
• Tarski's influence on computer science
• Automated Reasoning
• Logic Programming
• Find, use, and conserve tools for formal methods
• Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)

This page was built for publication: Little engines of proof

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