Orthologic with Axioms

on YouTube ↗20m

" summary

Presents orthologic extended with axioms and proves a generalized cut‑elimination and subformula property that yields a concrete decision procedure: provability from axioms (validity in finitely presented ortholattices) runs in cubic time, while syntactic normalization of single formulas is quadratic. Shows propositional resolution of width 5 suffices for all provable formulas, and that the system subsumes width‑2 resolution and arbitrary unit resolution. Extends to an EPR‑style effectively propositional orthologic that is decidable and FPT (runtime exponential only in the max variables per axiom), giving a Datalog generalization with negation and disjunction.

AI-written summary · about

" chapters (20)

1. 0:00Orthologic introduction
2. 3:12What is orthologic
3. 5:38Extending with axioms
4. 7:27Proof system
5. 8:30Cut elimination
6. 9:12Cubic-time proof search
7. 10:13Horn closures equivalence
8. 10:58Predicate orthologic
9. 12:02Orthologic vs Datalog
10. 12:46Summary and applications
11. 13:27Q&A: Models
12. 14:10Q&A: Reading orthologic formulas intuitively
13. 14:32Q&A: Implication connective
14. 14:53Q&A: Intuition
15. 15:41Q&A: Sequent restrictions
16. 16:24Q&A: Classical logic
17. 17:05Q&A: Performance
18. 17:47Q&A: Effect algebras
19. 18:09Q&A: Counterexamples
20. 18:51Q&A: SMT solver link