Online Otter-λ

Examples

Theorem: The composition of group homomorphims is a homomorphism.

This example illustrates that beta reduction works well with paramodulation.

The composition of two functions f and g is expressed as the lambda term lambda(x,f(g(x))). The verification that the composition of homomorphisms is a homomorphism is a straightforward piece of equational reasoning. However, we also need to prove that if Phi maps G to H and Psi maps H to K then the composition maps G to K. In this file, the groups G, H, and K are given by "propositional functions", that is, G, H, and K are treated as constants, and "x belongs to G" is represented by Ap(G,x) = $T. ($T means "true").

This theorem illustrates how lambda logic can sometimes make it very easy to formulate a precise version of a theorem that is rather difficult to formulate in set theory or in a first-order algebraic theory. Wick and McCune [1] showed how to formulate and prove this theorem in set theory. It was quite difficult.

[1] Wick, C., and McCune, W., Automated reasoning about elementary point-set topology, J. Automated Reasoning 5(2) 239-255, 1989.