Lazy techniques for fully expansive theorem proving

DOI10.1007/BF01383983zbMath0785.68077MaRDI QIDQ1309245

Richard J. Boulton

Publication date: 20 April 1994

Published in: Formal Methods in System Design (Search for Journal in Brave)

zbMATH Keywords

optimizationHOL theorem proverdelayed computationlazy conversionlazy theoremprimitive inference

Mathematics Subject Classification ID

Uses Software

• Unnamed Item
• HOL
• Nuprl
• NQTHM

Cites Work

• A higher-order implementation of rewriting
• Experiments with proof plans for induction
• Edinburgh LCF. A mechanized logic of computation
• A formulation of the simple theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Lazy techniques for fully expansive theorem proving