4.2 Article

The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions

相关参考文献

注意:仅列出部分参考文献,下载原文获取全部文献信息。
Article Computer Science, Software Engineering

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

Quang-Trung Ta et al.

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL (2018)

Proceedings Paper Automation & Control Systems

A Cut-Free Cyclic Proof System for Kleene Algebra

Anupam Das et al.

AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2017 (2017)

Proceedings Paper Computer Science, Software Engineering

Cyclic Arithmetic Is Equivalent to Peano Arithmetic

Alex Simpson

FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2017) (2017)

Article Mathematics

Circular proofs for the Godel-Lob provability logic

D. S. Shamkanov

MATHEMATICAL NOTES (2014)

Article Computer Science, Artificial Intelligence

Conjecture Synthesis for Inductive Theories

Moa Johansson et al.

JOURNAL OF AUTOMATED REASONING (2011)

Article Computer Science, Theory & Methods

Sequent calculi for induction and infinite descent

James Brotherston et al.

JOURNAL OF LOGIC AND COMPUTATION (2011)

Article Computer Science, Software Engineering

Cyclic proofs of program termination in separation logic

James Brotherston et al.

ACM SIGPLAN NOTICES (2008)

Article

Cut-free sequent systems for temporal logic

Kai Bruennler et al.

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING (2008)

Article Mathematics, Applied

Descente infinie plus deduction

Claus-Peter Wirth

LOGIC JOURNAL OF THE IGPL (2004)

Article Computer Science, Theory & Methods

Cut-elimination for a logic with definitions and induction

R McDowell et al.

THEORETICAL COMPUTER SCIENCE (2000)