Abstract is missing.
- A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTLLuca Geatti, Nicola Gigante, Angelo Montanari. 3-20 [doi]
- Certification of Nonclausal Connection Tableaux ProofsMichael Färber 0002, Cezary Kaliszyk. 21-38 [doi]
- ALCKatarina Britz, Ivan Varzinczak. 39-57 [doi]
- A Tableau Calculus for Non-clausal Maximum SatisfiabilityChu Min Li, Felip Manyà, Joan Ramon Soler. 58-73 [doi]
- First-Order Quasi-canonical Proof SystemsYotam Dvir, Arnon Avron. 77-93 [doi]
- Bounded Sequent Calculi for Non-classical Logics via HypersequentsAgata Ciabattoni, Timo Lang, Revantha Ramanayake. 94-110 [doi]
- A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional LogicCamillo Fiorentini, Rajeev Goré, Stéphane Graham-Lengrand. 111-129 [doi]
- Relating Labelled and Label-Free Bunched Calculi in BI LogicDidier Galmiche, Michel Marti, Daniel Méry. 130-146 [doi]
- Sequentialising Nested SystemsElaine Pimentel, Revantha Ramanayake, Björn Lellmann. 147-165 [doi]
- A Hypersequent Calculus with Clusters for Data Logic over OrdinalsAnthony Lick. 166-184 [doi]
- Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested SequentsRajeev Goré, Björn Lellmann. 185-202 [doi]
- Combining Monotone and Normal Modal Logic in Nested Sequents - with CountermodelsBjörn Lellmann. 203-220 [doi]
- On Combinatorial Proofs for Modal LogicMatteo Acclavio, Lutz Straßburger. 223-240 [doi]
- A Game Model for Proofs with CostsTimo Lang, Carlos Olarte, Elaine Pimentel, Christian G. Fermüller. 241-258 [doi]
- Towards a Combinatorial Proof TheoryBenjamin Ralph, Lutz Straßburger. 259-276 [doi]
- Birkhoff Completeness for Hybrid-Dynamic First-Order LogicDaniel Gâinâ, Ionut Tutu. 277-293 [doi]
- Infinets: The Parallel Syntax for Non-wellfounded Proof-TheoryAbhishek De, Alexis Saurin. 297-316 [doi]
- PSPACE-Completeness of a Thread Criterion for Circular Proofs in Linear Logic with Least and Greatest Fixed PointsRémi Nollet, Alexis Saurin, Christine Tasson. 317-334 [doi]
- A Non-wellfounded, Labelled Proof System for Propositional Dynamic LogicSimon Docherty, Reuben N. S. Rowe. 335-352 [doi]
- Herbrand Constructivization for Automated Intuitionistic Theorem ProvingGabriel Ebner. 355-373 [doi]
- ENIGMAWatch: ProofWatch Meets ENIGMAZarathustra Goertzel, Jan Jakubuv, Josef Urban. 374-388 [doi]
- Behavioral Program LogicEduard Kamburjan. 391-408 [doi]
- Prenex Separation Logic with One Selector FieldMnacho Echenim, Radu Iosif, Nicolas Peltier. 409-427 [doi]
- Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical SystemsJoão G. Martins, André Platzer, João Leite. 428-445 [doi]
- Operational Semantics and Program Verification Using Many-Sorted Hybrid Modal LogicIoana Leustean, Natalia Moanga, Traian-Florin Serbanuta. 446-476 [doi]