pytableaux 2.3.3
Argument
C
Load example argument ...
Addition
Affirming a Disjunct 1
Affirming a Disjunct 2
Affirming the Consequent
Asserted Addition
Assertion Elimination 1
Assertion Elimination 2
Biconditional Elimination 1
Biconditional Elimination 2
Biconditional Elimination 3
Biconditional Identity
Biconditional Introduction 1
Biconditional Introduction 2
Biconditional Introduction 3
Conditional Contraction
Conditional Contraposition 1
Conditional Contraposition 2
Conditional Double Negation
Conditional Equivalence
Conditional Identity
Conditional Law of Excluded Middle
Conditional Modus Ponens
Conditional Modus Tollens
Conditional Pseudo Contraction
Conditional Pseudo Contraposition
Conjunction Commutativity
Conjunction Elimination
Conjunction Introduction
Conjunction Pseudo Commutativity
DeMorgan 1
DeMorgan 2
DeMorgan 3
DeMorgan 4
DeMorgan 5
DeMorgan 6
DeMorgan 7
DeMorgan 8
Denying the Antecedent
Disjunction Commutativity
Disjunction Pseudo Commutativity
Disjunctive Syllogism 2
Disjunctive Syllogism
Existential from Universal
Existential Syllogism
Explosion
Extracting a Disjunct 1
Extracting a Disjunct 2
Extracting the Antecedent
Extracting the Consequent
Identity Indiscernability 1
Identity Indiscernability 2
KFDE Distribution Inference 1
Law of Excluded Middle
Law of Non-contradiction
Material Biconditional Elimination 1
Material Biconditional Elimination 2
Material Biconditional Elimination 3
Material Biconditional Identity
Material Biconditional Introduction 1
Material Contraction
Material Contraposition 1
Material Contraposition 2
Material Identity
Material Modus Ponens
Material Modus Tollens
Material Pseudo Contraction
Material Pseudo Contraposition
Modal Platitude 1
Modal Platitude 2
Modal Platitude 3
Modal Transformation 1
Modal Transformation 2
Modal Transformation 3
Modal Transformation 4
Necessity Distribution 1
Necessity Distribution 2
Necessity Elimination
NP Collapse 1
NP Conditional Modus Ponens
Possibility Addition
Possibility Distribution
Quantifier Interdefinability 1
Quantifier Interdefinability 2
Quantifier Interdefinability 3
Quantifier Interdefinability 4
Reflexive Inference 1
S4 Conditional Inference 1
S4 Conditional Inference 2
S4 Material Inference 1
S4 Material Inference 2
S5 Conditional Inference 1
S5 Inference 1
S5 Material Inference 1
Self Identity 1
Self Identity 2
Serial Inference 1
Serial Inference 2
Syllogism
Triviality 1
Triviality 2
Universal from Existential
Universal Predicate Syllogism
Logic
CPL
CFOL
K
D
T
S4
S5
FDE
K3
LP
L3
RM3
K3W
K3WQ
B3E
G3
MH
NH
GO
P3
KFDE
TFDE
S4FDE
S5FDE
KK3
TK3
S4K3
S5K3
KLP
TLP
S4LP
S5LP
KL3
TL3
S4L3
S5L3
KRM3
TRM3
S4RM3
S5RM3
KK3W
TK3W
S4K3W
S5K3W
KB3E
TB3E
S4B3E
S5B3E
KG3
TG3
S4G3
S5G3
S4GO
Bochvar 3 External Logic
quantified
many-valued
gappy
Classical First Order Logic
quantified
bivalent
Classical Predicate Logic
bivalent
Deontic Normal Modal Logic
quantified
bivalent
modal
First Degree Entailment
quantified
many-valued
gappy
glutty
Gödel 3-valued Logic
quantified
many-valued
gappy
Gappy Object Logic
quantified
many-valued
gappy
Kripke Normal Modal Logic
quantified
bivalent
modal
Strong Kleene Logic
quantified
many-valued
gappy
Weak Kleene Logic
quantified
many-valued
gappy
Weak Kleene alt-Q Logic
quantified
many-valued
gappy
B3E with K modal
quantified
many-valued
gappy
modal
FDE with K modal
quantified
many-valued
gappy
glutty
modal
G3 with K modal
quantified
many-valued
gappy
modal
K3 with K modal
quantified
many-valued
gappy
modal
K3W with K modal
quantified
many-valued
gappy
modal
L3 with K modal
quantified
many-valued
gappy
modal
LP with K modal
quantified
many-valued
gappy
glutty
modal
RM3 with K modal
quantified
many-valued
gappy
glutty
modal
Łukasiewicz 3-valued Logic
quantified
many-valued
gappy
Logic of Paradox
quantified
many-valued
gappy
glutty
Paracomplete Hybrid Logic
many-valued
gappy
Paraconsistent Hybrid Logic
many-valued
gappy
glutty
Post 3-valued Logic
many-valued
gappy
R-mingle 3
quantified
many-valued
gappy
glutty
S4 Normal Modal Logic
quantified
bivalent
modal
B3E with S4 modal
quantified
many-valued
gappy
modal
FDE with S4 modal
quantified
many-valued
gappy
glutty
modal
G3 with S4 modal
quantified
many-valued
gappy
modal
GO S4 modal logic
quantified
many-valued
gappy
modal
K3 with S4 modal
quantified
many-valued
gappy
modal
K3W with S4 modal
quantified
many-valued
gappy
modal
L3 with S4 modal
quantified
many-valued
gappy
modal
LP with S4 modal
quantified
many-valued
gappy
glutty
modal
RM3 with S4 modal
quantified
many-valued
gappy
glutty
modal
S5 Normal Modal Logic
quantified
bivalent
modal
B3E with S5 modal
quantified
many-valued
gappy
modal
FDE with S5 modal
quantified
many-valued
gappy
glutty
modal
G3 with S5 modal
quantified
many-valued
gappy
modal
K3 with S5 modal
quantified
many-valued
gappy
modal
K3W with S5 modal
quantified
many-valued
gappy
modal
L3 with S5 modal
quantified
many-valued
gappy
modal
LP with S5 modal
quantified
many-valued
gappy
glutty
modal
RM3 with S5 modal
quantified
many-valued
gappy
glutty
modal
Reflexive Normal Modal Logic
quantified
bivalent
modal
B3E with T modal
quantified
many-valued
gappy
modal
FDE with T modal
quantified
many-valued
gappy
glutty
modal
G3 with T modal
quantified
many-valued
gappy
modal
K3 with T modal
quantified
many-valued
gappy
modal
K3W with T modal
quantified
many-valued
gappy
modal
L3 with T modal
quantified
many-valued
gappy
modal
LP with T modal
quantified
many-valued
gappy
glutty
modal
RM3 with T modal
quantified
many-valued
gappy
glutty
modal
Symbols
Operators
T
⚬
Assertion
N
¬
Negation
K
∧
Conjunction
A
∨
Disjunction
C
⊃
Material Conditional
E
≡
Material Biconditional
U
→
Conditional
B
↔
Biconditional
M
◇
Possibility
L
◻
Necessity
Operators
*
⚬
Assertion
~
¬
Negation
&
∧
Conjunction
V
∨
Disjunction
>
⊃
Material Conditional
<
≡
Material Biconditional
$
→
Conditional
%
↔
Biconditional
P
◇
Possibility
N
◻
Necessity
Atomics
a
b
c
d
e
Constants
m
n
o
s
Variables
x
y
z
v
Quantifiers
S
∃
Existential
V
∀
Universal
Atomics
A
B
C
D
E
Constants
a
b
c
d
Variables
x
y
z
v
Quantifiers
X
∃
Existential
L
∀
Universal
Predicates
F
G
H
O
F
G
H
O
J
!
E!
Existence
I
=
=
Identity
Input Notation
polish
standard
Output Format
html
latex
text
Output Notation
polish
standard
Show Controls
Build Models
Color Open
Max Steps