Using tactics to reformulate formulae for resolution theorem proving

DOI10.1007/BF02127748zbMath0891.68094MaRDI QIDQ1380410

Manfred Kerber, Axel Präcklein

Publication date: 4 March 1998

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

resolution-based theorem proving systems

Mathematics Subject Classification ID

Related Items (1)

Automating change of representation for proofs in discrete mathematics (extended version)

Uses Software

• ETPS
• Nuprl
• LCF
• MKRP
• CLAM
• Oyster

Cites Work

• Seventy-five problems for testing automatic theorem provers
• Splitting and reduction heuristics in automatic theorem proving
• A formulation of the simple theory of types
• Completeness in the theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Using tactics to reformulate formulae for resolution theorem proving