Transitivity : syntactic
Extensionality
Extensionality
Causal invariance in metamathematics
Causal invariance in metamathematics
[ If strongly normalizing (= every rewrite sequence reaches normal form), then confluence implies: everything easy ]
FindEquationalProof :
if the system is confluent, any path in the equational multiway system will work (apart from the infinity problem)
if the system is confluent, any path in the equational multiway system will work (apart from the infinity problem)
Given confluence, algorithm to prove a theorem is trivial , but may take a long time to run
[ algorithm to find an optimal proof may be nontrivial ]
[ algorithm to find an optimal proof may be nontrivial ]
Representations of math
Representations of math
FindEquationalProof
FindEquationalProof
Is only inbuilt predicate
Predicate logic:
implies[x,y]
FindEquationalProof[implies[a,c],{ForAll[implies[