Cyclist

swMATH18519MaRDI QIDQ30358FDOQ30358

Author name not available (Why is that?)

Source code repository: https://github.com/ngorogiannis/cyclist

Cited In (26)

• Uniform interpolation from cyclic proofs: the case of modal mu-calculus
• Circular proofs for the Gödel-Löb provability logic
• Model checking for symbolic-heap separation logic with inductive predicates
• Disproving inductive entailments in separation logic via base pair approximation
• Title not available (Why is that?)
• Local validity for circular proofs in linear logic with fixed points
• Transforming orthogonal inductive definition sets into confluent term rewrite systems
• Program Verification with Separation Logic
• Title not available (Why is that?)
• Soundness and completeness proofs by coinductive methods
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Cyclic arithmetic is equivalent to Peano arithmetic
• PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
• Program equivalence is coinductive
• Automated mutual induction proof in separation logic
• Compositional entailment checking for a fragment of separation logic
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Partial evaluation of string obfuscations for Java malware detection
• Clause set cycles and induction
• Induction and Skolemization in saturation theorem proving
• Cyclic proofs, hypersequents, and transitive closure logic
• Deciding entailments in inductive separation logic with tree automata
• Sound and complete equational reasoning over comodels
• Combining induction and saturation-based theorem proving
• Inductive theorem proving based on tree grammars
• Unified reasoning about robustness properties of symbolic-heap separation logic

This page was built for software: Cyclist