Behavioral Program Logic

First-order Quasi-canonical Proof Systems

Bounded sequent calculi for non-classical logics via hypersequents

On Combinatorial Proofs for Modal Logic

A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL

A Game Model for Proofs with Costs

Certification of Nonclausal Connection Tableaux Proofs

intuit implements LJT

Relating Labelled and Label-Free Bunched Calculi in BI Logic

Prenex Separation Logic with One Selector Field

Infinets: The parallel syntax for non-wellfounded proof-theory

Sequentialising nested systems

Herbrand constructivization for automated intuitionistic theorem proving

A Hypersequent Calculus with Clusters for Data Logic over Ordinals

Tableau-based translation from first-order logic to modal logic

Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems

Towards a Combinatorial Proof Theory

Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents

PSPACE-Completeness of a Thread Criterion for Circular Proofs in Linear Logic with Least and Greatest Fixed Points

Operational semantics and program verification (using many-sorted hybrid modal logic)

Combining monotone and normal modal logic in nested sequents -- with countermodels

A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic

Birkhoff Completeness for Hybrid-Dynamic First-Order Logic

Preferential Tableaux for Contextual Defeasible ALC

A Tableau Calculus for Maximum Satisfiability

ENIGMAWatch: ProofWatch Meets ENIGMA