Lew Gordeew, WSI f. Informatik, Tuebingen University

Quantified Propositional Logic (QPL). Part 1.

This is the first part of my presentation of QPL theory. It entails main definitions of syntax and semantics and basic proof systems (both classical and intuitionistic). Various soundness and completeness proofs (both tree-like and dag-like, with and without compression) and related numerical estimates will be presented and discussed; the intuitionistic completeness corresponds to the cut elimination theorem. Analogous results concerning proof systems extended by the substitution rule will be presented and discussed as well (if time allows).

Stronger DAG Compression

We add a new (valid) strong propositional substitution rule (SUB) : $\frac{\Gamma}{\theta(\Gamma)}$ for any $\theta \in \mbox{Hom}(V~AR \to F0R)$ and consider dag-like cut-free sequent calculus SEQ$_{sub}$ with (SUB) (for brevity classical, but also keep intuitionistic one in mind). We formulate for SEQ$_{sub}$ the Hauptsatz with Compression. We ask if SEQ$_{sub}$ admits better/faster speed-up of proof compression than analogous calculus with weaker substitution for $\theta \in \mbox{Hom}(V~AR \to LIT)$?

Talk on Monday (29/07/2013)

Basic DAG Compression Theory - Part I

TecMF: TalksLew2013 (last edited 2014-10-16 13:13:22 by BrunoLopes)