# A Cyclic Proof System for HFL_ℕ

@inproceedings{Kori2021ACP, title={A Cyclic Proof System for HFL\_ℕ}, author={Mayuko Kori and Takeshi Tsukada and Naoki Kobayashi}, booktitle={CSL}, year={2021} }

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… Expand

#### 2 Citations

An Overview of the HFL Model Checking Project

- Computer Science
- HCVS@ETAPS
- 2021

This article presents its methods for automatically solving the HFL(Z) model/validity checking problems, using higher-order model checkers and CHC solvers as backends. Expand

A Cyclic Proof System for HFLN

- Computer Science
- ArXiv
- 2020

This work proposes a cyclic proof system for HFLN, which is a higher-order predicate logic with natural numbers and alternating fixed-points, and proves the decidability of checking the global condition and soundness of this system, and also proves a restricted form of standard completeness for an infinitary variant of the system. Expand

#### References

SHOWING 1-10 OF 17 REFERENCES

Reduction from branching-time property verification of higher-order programs to HFL validity checking

- Computer Science
- PEPM@POPL
- 2019

This paper formalizes branching-time property verification problems as an extension of HORS model checking called HORSZ model checking, presents a sound and complete reduction to validity checking of (modal-free) HFLZ formulas, and proves the correctness of the reduction. Expand

Temporal Verification of Programs via First-Order Fixpoint Logic

- Computer Science
- SAS
- 2019

The method generalizes a reduction from termination verification to safety property verification and reduces validity of a Mu-Arithmetic formula to satisfiability of CHC, which can then be solved by using off-the-shelf CHC solvers. Expand

Higher-Order Program Verification via HFL Model Checking

- Computer Science
- ESOP
- 2018

This paper shows that various verification problems for functional programs, including may/must-reachability, trace properties, and linear-time temporal properties (and their negations), can be naturally reduced to (extended) HFL model checking. Expand

Higher-order constrained horn clauses for verification

- Computer Science
- Proc. ACM Program. Lang.
- 2018

It is shown that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained through a reduction to a problem concerning a kind of monotone logic program. Expand

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

- Computer Science
- CADE
- 2017

A proof system whose judgements express that a program has a certain temporal property over memory state assertions in separation logic, and whose rules operate directly on the temporal modalities as well as symbolically executing programs. Expand

On the infinitary proof theory of logics with fixed points. (Théorie de la démonstration infinitaire pour les logiques à points fixes)

- Mathematics, Computer Science
- 2017

It is argued that infinitary proofs have a true proof-theoretical status by showing that the multiplicative additive linear-logic with fixed points admits focalization and cut-elimination. Expand

On the relationship between higher-order recursion schemes and higher-order fixpoint logic

- Computer Science
- POPL 2017
- 2017

To prove the correctness of the translation from HORS to HFL model checking, it is shown that there exist (arguably) natural reductions between the two problems, enabling cross-fertilization of the two research threads. Expand

A Type-Directed Negation Elimination

- Mathematics, Computer Science
- FICS
- 2015

This paper presents a procedure that converts a formula into an equivalent formula without negations of quadratic size in the worst case and of linear size when the number of variables of the formula is fixed. Expand

Alternating Parity Krivine Automata

- Computer Science
- MFCS
- 2014

An automaton model is presented that captures the semantics of HFL, a non-regular extension of the modal μ-calculus by a typed λ-Calculus that combines alternating parity automata with the lookup mechanisms from the Krivine machine. Expand

A Generic Cyclic Theorem Prover

- Computer Science
- APLAS
- 2012

The design and implementation of an automated theorem prover realising a fully general notion of cyclic proof, able to construct proofs obeying a very general cycle scheme, and to verify the general, global infinitary condition on such proof objects ensuring their soundness. Expand