Brotherston, J;
Gorogiannis, N;
Petersen, RL;
(2012)
A generic cyclic theorem prover.
In:
Asian Symposium on Programming Languages and Systems APLAS 2012: Programming Languages and Systems.
(pp. pp. 350-367).
Springer: Berlin, Heidelberg.
Preview |
Text
cyclist_APLAS-new.pdf - Published Version Download (224kB) | Preview |
Abstract
We describe the design and implementation of an automated theorem prover realising a fully general notion of cyclic proof. Our tool, called CYCLIST, is able to construct proofs obeying a very general cycle scheme in which leaves may be linked to any other matching node in the proof, and to verify the general, global infinitary condition on such proof objects ensuring their soundness. CYCLIST is based on a new, generic theory of cyclic proofs that can be instantiated to a wide variety of logics. We have developed three such concrete instantiations, based on: (a) first-order logic with inductive definitions; (b) entailments of pure separation logic; and (c) Hoare-style termination proofs for pointer programs. Experiments run on these instantiations indicate that CYCLIST offers significant potential as a future platform for inductive theorem proving. © Springer-Verlag Berlin Heidelberg 2012.
| Type: | Proceedings paper |
|---|---|
| Title: | A generic cyclic theorem prover |
| Event: | Programming Languages and Systems. APLAS 2012 |
| ISBN: | 978-3-642-35181-5 |
| ISBN-13: | 978-3-642-35182-2 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-642-35182-2_25 |
| Publisher version: | https://doi.org/10.1007/978-3-642-35182-2_25 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10140071 |
Archive Staff Only
 |
View Item |
