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

Julian Richardson; Alan Smaill; Ian Green

doi:10.1007/BFb0054254

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

Julian Richardson, Alan Smaill, Ian Green

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
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
Pages	129-133
Number of pages	5
ISBN (Electronic)	978-3-540-69110-5
ISBN (Print)	978-3-540-64675-4
DOIs	https://doi.org/10.1007/BFb0054254
Publication status	Published - 1998

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	1421
ISSN (Print)	0302-9743

Access to Document

10.1007/BFb0054254

http://link.springer.com/chapter/10.1007/BFb0054254

Cite this

Richardson, J., Smaill, A., & Green, I. (1998). System description: Proof planning in higher-order logic with $Clam. In Automated Deduction—CADE-15: 15th International Conference on Automated Deduction Lindau, Germany, July 5–10, 1998 Proceedings (pp. 129-133). (Lecture Notes in Computer Science; Vol. 1421). Springer Berlin Heidelberg. https://doi.org/10.1007/BFb0054254

@inproceedings{c68ade9cc11749418fbb105487bafea6,

title = "System description: Proof planning in higher-order logic with $Clam",

abstract = "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.",

author = "Julian Richardson and Alan Smaill and Ian Green",

year = "1998",

doi = "10.1007/BFb0054254",

language = "English",

isbn = "978-3-540-64675-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "129--133",

booktitle = "Automated Deduction—CADE-15",

}

System description: Proof planning in higher-order logic with $Clam. / Richardson, Julian; Smaill, Alan; Green, Ian.

Automated Deduction—CADE-15: 15th International Conference on Automated Deduction Lindau, Germany, July 5–10, 1998 Proceedings. Springer Berlin Heidelberg, 1998. p. 129-133 (Lecture Notes in Computer Science; Vol. 1421).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Richardson, Julian

AU - Smaill, Alan

AU - Green, Ian

PY - 1998

Y1 - 1998

N2 - 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.

AB - 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.

U2 - 10.1007/BFb0054254

DO - 10.1007/BFb0054254

M3 - Conference contribution

SN - 978-3-540-64675-4

T3 - Lecture Notes in Computer Science

SP - 129

EP - 133

BT - Automated Deduction—CADE-15

PB - Springer Berlin Heidelberg

ER -

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

Abstract

Publication series

Access to Document

Fingerprint

Cite this