We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: A Cyclic Proof System for HFLN

Abstract: A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFLN, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.'s recent work on reductions from program verification to HFLN validity checking.
Comments: 27 pages
Subjects: Logic in Computer Science (cs.LO); Computation and Language (cs.CL)
MSC classes: 03B70
Cite as: arXiv:2010.14891 [cs.LO]
  (or arXiv:2010.14891v1 [cs.LO] for this version)

Submission history

From: Mayuko Kori [view email]
[v1] Wed, 28 Oct 2020 11:19:53 GMT (64kb,D)

Link back to: arXiv, form interface, contact.