Some Useful Commands in TPS (2008)
Peter B. Andrews, Peter B. Andrews, Eve Longini Cohen, Dale A. Miller, Ph. D, Dan Nesmith, ...
[ ∼ A] means “A is not true”; [A ∧ B] means “A and B”; [A ∨ B] means “A or B”; [A ⊃ B] means “A implies B”; [A ≡ B] means “A if and only if B”; When the relative scopes...
Theorem proving in type theory (1977)
Peter B. Andrews, Eve Longini Cohen
As one aspect of the endeavor to create new intellectual tools for mankind, we wish to enable computers to prove, and to assist in the proofs of, theorems of mathematics and (eventually) other...