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:
φ:
ψ:
χ:
Contradiction Realization:
(~φ => ψ) => ((~φ => ~ψ) => φ)
Enter values for the meta-variables in the schema:
φ:
ψ:
Universal Instantiation:
Aν:φ => φ[ν←τ]
where τ is free for ν in φ.
Enter values for the meta-variables in the schema:
ν:
φ:
τ:
Universal Distribution:
Aν:(φ => ψ) => (φ => Aν:ψ)
where ν does not occur free in φ.
Enter values for the meta-variables in the schema:
ν:
φ:
ψ:
Universal Generalization:
φ
Aν:φ
Enter the variable you would like to use:
ν:
© 2001-2007 Stanford University Logic Group. All rights reserved.
Comments to
Michael Genesereth
.