@article(Berardi:2019aa,
author = {S. Berardi and M. Tatsuta},
year = {2019},
title = {Classical System of {M}artin-{L}of's Inductive Definitions is not Equivalent to Cyclic Proofs},
journal = {Logical Methods in Computer Science},
volume = {15},
number = {3},
doi = {10.23638/LMCS-15(3:10)2019},
)
@inproceedings(Brotherston:2005qy,
author = {J. Brotherston},
year = {2005},
title = {Cyclic Proofs for First-Order Logic with Inductive Definitions},
booktitle = {Proceedings of {TABLEAUX-14}},
series = {LNAI},
volume = {3702},
publisher = {Springer-Verlag},
pages = {78--92},
doi = {10.1007/11554554_8},
)
@phdthesis(Brotherston:2006uy,
author = {J. Brotherston},
year = {2006},
title = {Sequent Calculus Proof Systems for Inductive Definitions},
school = {University of Edinburgh},
)
@inproceedings(Brotherston:2012fk,
author = {J. Brotherston and N. Gorogiannis and R. L. Petersen},
year = {2012},
title = {A Generic Cyclic Theorem Prover},
booktitle = {APLAS-10 (10th Asian Symposium on Programming Languages and Systems)},
series = {LNCS},
volume = {7705},
publisher = {Springer},
pages = {350--367},
doi = {10.1007/978-3-642-35182-2_25},
)
@article(Brotherston:2011fk,
author = {J. Brotherston and A. Simpson},
year = {2011},
title = {Sequent calculi for induction and infinite descent},
journal = {Journal of Logic and Computation},
volume = {21},
number = {6},
pages = {1177--1216},
doi = {10.1093/logcom/exq052},
)
@article(Dershowitz:2007bf,
author = {N. Dershowitz and G. Moser},
year = {2007},
title = {The {H}ydra Battle Revisited},
journal = {Rewriting, Computation and Proof},
pages = {1--27},
doi = {10.1007/978-3-540-73147-4\_1},
)
@article(Gentzen:1935fk,
author = {G. Gentzen},
year = {1935},
title = {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en. {I}},
journal = {Mathematische Zeitschrift},
volume = {39},
pages = {176--210},
doi = {10.1007/BF01201353},
)
@techreport(Michel:1988aa,
author = {M. Michel},
year = {1988},
title = {Complementation is more difficult with automata on infinite words},
type = {Technical Report},
institution = {CNET},
)
@inproceedings(Stratulat:2017ac,
author = {S. Stratulat},
year = {2017},
title = {Cyclic Proofs with Ordering Constraints},
editor = {R. A. Schmidt and C. Nalon},
booktitle = {TABLEAUX 2017 (26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods)},
series = {LNAI},
volume = {10501},
publisher = {Springer},
pages = {311--327},
doi = {10.1007/978-3-319-66902-1_19},
)
@inproceedings(Stratulat:2018ab,
author = {S. Stratulat},
year = {2018},
title = {Validating Back-links of {FOL}$_{\unhbox\voidb@x \hbox{\uppercase{{ID}}}}$ Cyclic Pre-proofs},
editor = {S. Berardi and S. van Bakel},
booktitle = {CL\&C'18 (Seventh International Workshop on Classical Logic and Computation)},
series = {{EPTCS}},
volume = {281},
pages = {39--53},
doi = {10.4204/EPTCS.281.4},
)