Logica
Truth Table
Clausal Form
Unification
Transformation
Deduction
Resolution
Epilog
Step
Proof
Justification
Enter the premise you wish to add to the proof:
Implication Introduction:
φ => (ψ => φ)
Enter values for the meta-variables in the schema:
φ:
ψ:
Implication Distribution:
(φ => (ψ => χ)) => ((φ => ψ) => (φ => χ))
Enter values for the meta-variables in the schema:
φ:
ψ:
χ:
And Introduction:
φ => (ψ => φ ∧ ψ)
Enter values for the meta-variables in the schema:
φ:
ψ:
And Elimination I:
φ ∧ ψ => φ
Enter values for the meta-variables in the schema:
φ:
ψ:
And Elimination II:
φ ∧ ψ => ψ
Enter values for the meta-variables in the schema:
φ:
ψ:
Or Introduction I:
φ => φ ∨ ψ
Enter values for the meta-variables in the schema:
φ:
ψ:
Or Introduction II:
ψ => φ ∨ ψ
Enter values for the meta-variables in the schema:
φ:
ψ:
Or Elimination:
(φ => χ) => ((ψ => χ) => (φ ∨ ψ => χ))
Enter values for the meta-variables in the schema:
φ:
ψ:
χ:
Contradiction Realization:
(φ => ψ) => ((φ => ~ψ) => ~φ)
Enter values for the meta-variables in the schema:
φ:
ψ:
Double Negation:
~~φ => φ
Enter a value for the meta-variable in the schema:
φ:
© 2001-2007 Stanford University Logic Group. All rights reserved.
Comments to
Michael Genesereth
.