5 papers
Uniform Lyndon Interpolation via Non-wellfounded Proofs
Borja Sierra Miranda, Thomas Studer
Non-wellfounded proof theory has been applied to establish uniform interpolation and Lyndon interpolation (separately) for multiple logics. However, it has not yet been used to pro…
Cyclic Proofs for iGL via Corecursion
Borja Sierra Miranda
Cyclic proof theory studies proofs where cycles are allowed. This is useful for developing proof theory for logics with fixpoint operators: cycles can be used to represent the unfo…
Knowledge and Common Knowledge of Strategies
Borja Sierra Miranda, Thomas Studer
Most existing work on strategic reasoning simply adopts either an informed or an uninformed semantics. We propose a model where knowledge of strategies can be specified on a fine-g…
Coalgebraic proof translations for non-wellfounded proofs
Borja Sierra Miranda, Thomas Studer, Lukas Zenger
Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constra…
Algebraic Proof Theory for Infinitary Action Logic
Wesley Fussner, Simon Santschi, Borja Sierra Miranda
We exhibit a uniform method for obtaining (wellfounded and non-wellfounded) cut-free sequent-style proof systems that are sound and complete for various classes of action algebras,…