This system description outlines the λClam system for proof planning in higher-order logic. The usefulness and feasibility of applying higher-order proof planning to a number of types of problem is outlined, in particular the synthesis and verification of software and hardware systems. The use of a higher-order metatheory overcomes problems encountered in Clam because of its inability to reason properly about higher-order objects. λClam is written in λProlog.
|Title of host publication||Automated Deduction—CADE-15|
|Subtitle of host publication||15th International Conference on Automated Deduction Lindau, Germany, July 5–10, 1998 Proceedings|
|Publisher||Springer Berlin Heidelberg|
|Number of pages||5|
|Publication status||Published - 1998|
|Name||Lecture Notes in Computer Science|
|Publisher|| Springer Berlin Heidelberg|