Logica
Truth Table
Clausal Form
Unification
Transformation
Deduction
Resolution
Epilog
Step
Proof
Justification
Enter the premise you wish to add to the proof:
Universal Instantiation:
Aν:φ
φ[ν←τ]
where τ is free for ν in φ
Enter the term you would like to use:
τ:
Existential Instantiation:
Eν:φ
φ[ν←τ]
where Eν:φ contains no free variables
Enter the term you would like to use:
τ:
Universal Generalization:
φ
Aν:φ
Enter the variable you would like to use:
ν:
Existential Generalization:
φ(τ)
Eν:φ(ν)
Enter the term you would like to replace:
τ:
Enter the variable you would like to use:
ν:
© 2001-2007 Stanford University Logic Group. All rights reserved.
Comments to
Michael Genesereth
.