Orthologic with Axioms - Proof Theory and Algorithms

Explore a 20-minute video presentation from POPL 2024 on Orthologic with Axioms by Simon Guilloud and Viktor Kunčak from EPFL, Switzerland. Delve into the proof theory and algorithms for orthologic, a logical system based on ortholattices with practical applications in verification condition simplification and normalization. Discover how the researchers generalize ortholattice reasoning to prove a broader class of classically valid formulas. Examine the key analysis of a proof system for orthologic augmented with axioms, featuring a limit of two formulas per sequent. Learn about the generalized form of cut elimination, which leads to a cubic-time algorithm for provability from axioms. Understand how orthologic with axioms subsumes certain forms of resolution and relates to propositional Horn clauses. Investigate the introduction of effectively propositional orthologic, its semantics, and a sound and complete proof system, which implies decidability and fixed-parameter tractability. Gain insights into a generalization of Datalog with negation and disjunction as a special case of this system.