System description: Proof planning in higher-order logic with $Clam

Julian Richardson, Alan Smaill, Ian Green

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationAutomated Deduction—CADE-15
Subtitle of host publication15th International Conference on Automated Deduction Lindau, Germany, July 5–10, 1998 Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages5
ISBN (Electronic)978-3-540-69110-5
ISBN (Print)978-3-540-64675-4
Publication statusPublished - 1998

Publication series

NameLecture Notes in Computer Science
Publisher Springer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'System description: Proof planning in higher-order logic with $Clam'. Together they form a unique fingerprint.

Cite this