Revision #918 → #1558 · back to history
addedSequent calculus33c87c64147a
addedHilbert stylebb294320cef0
addedGentzen stylea9721db0682f
addedNatural deduction3e9260334cd8
addedSequent calculus line form87c7825df693
addedGentzen's Hauptsatz (cut-elimination)7f7385b069a8
addedConsistency of Peano arithmetic11c3bc6e5214
addedHilbert-style judgment463d96cefb79
addedNatural deduction judgment043d7a433533
addedSemantics of natural deduction judgmente422b9ae5fd2
addedAntecedent and succedentc46201d99a78
addedSemantics of a sequentf326ad643b9d
addedEmpty sequent is false182ffe24f234
addedClassical reformulations of sequent semantics958fcb3f047c
addedReduction tree example formulaebadc802a543
addedReduction treec15126b701ab
addedAxiom condition for atomic sequentsfb5dbb2a0ae1
addedSoundness and completeness of reduction-tree systemd394873b2142
addedProvability via reduction trees69e84f8425ac
addedFormal proof in LK619259b91d0e
addedFree variable occurrencea494e43e1370
addedSubstitution notation27c55c818a61
addedStructural rule abbreviationsb056a39e4302
addedCut-elimination theorem3364bc35f434
addedCompleteness of atomic initial sequents6527c3d1878a
addedLaw of excluded middle derivation3c7ef824fda4
addedQuantifier fact derivationc1c55ef887c7
addedLK derivation showing automated proving03d491c3e8ae
addedSequent proof ↔ closed analytic tableau2631950d9ab8
addedWeakening rule95d791b659d1
addedContraction and Permutation7784176e4039
addedSubstructural logicsb1f46a3eb93b
addedSoundness and completeness of LK99e69bcc3ab2
addedAdmissibility of cut (Hauptsatz)ebe23e05c0f5
addedAdmissibility of weakening via modified axiom5cf79469df2a
addedAbsurdity constant8e1c115e7564
addedNegation from implication3ac30411bf39
addedSystem LJe04ee6ab443b
addedSoundness and completeness of LJadea44d23db0
addedDisjunction and existence properties9ad7e290763b