scientific article; zbMATH DE number 1956528

MaRDI QIDQ4417874zbMATH OpenFDO

Authors Christoph Sprenger, Mads Dam

Publication date 30 July 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2620/26200425.htm

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Structure of proofs (03F07) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On global induction mechanisms in aμ-calculus with explicit approximations
• On the proof theory of the modal mu-calculus
• Automated Reasoning with Analytic Tableaux and Related Methods
• Infinets: the parallel syntax for non-wellfounded proof-theory
• On the formalization of the modal -calculus in the calculus of inductive constructions

Cited in

(29)

• On the proof theory of the modal mu-calculus
• Cut elimination for a logic with induction and co-induction
• Non-well-founded deduction for induction and coinduction
• Integrating induction and coinduction via closure operators and proof cycles
• Uniform interpolation from cyclic proofs: the case of modal mu-calculus
• Infinets: the parallel syntax for non-wellfounded proof-theory
• Temporal refinements for guarded recursive types
• Cyclic arithmetic is equivalent to Peano arithmetic
• On global induction mechanisms in aμ-calculus with explicit approximations
• Size-based termination of higher-order rewriting
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
• Circular proofs as session-typed processes: a local validity condition
• The Recursion Scheme from the Cofree Recursive Comonad
• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• Well-founded recursion with copatterns and sized types
• Interactive programming in Agda -- objects and graphical user interfaces
• Compositional coinduction with sized types
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Constructing initial algebras using inflationary iteration
• Proof systems for the modal \(\mu \)-calculus obtained by determinizing automata
• From GTC to \textsc{Reset}: generating reset proof systems from cyclic proof systems
• A cyclic proof system for HFL\(_\mathbb{N}\)
• A unified view of induction reasoning for first-order logic
• Proof systems for two-way modal -calculus
• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
• A cyclic proof system for guarded Kleene algebra with tests
• Computation by infinite descent made explicit
• Types, Tableaus and Gödel’s God in Isabelle/HOL
• Canonical completeness of infinitary \(\mu \)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4417874)