[Albrecht Heeffer]
Home Logic Math Publications Shogi Sites About Me
         
Gentzen-style sequent calculus prover

Dorota Leszczyñska's Socratic proofs for modal logics

Example:

Choose a modal logic:
Logic: K D T KB K4 K5 DB D4 D5 B K45 D45 S4 S5

Press send for the proof of this example, or edit the input fields for a different problem
Some guidelines:
'-' is classic negation ¬
'@' is possible ◊
'#' is necessary
Always use a space before a '-' and '~'
For '◊◊p', use brackets: @(@ p)
use a space before and after disjunction ∨
The proof is shown using Gentzen-style sequents with a number indicating the level on which they appear


Based on: Dorota Leszczyñska (2004) "Socratic Proofs for Normal Modal Logics: A Right-sided Approach ", To appear. 
© 2005 Albrecht Heeffer and Dorota Leszczyñska