O'Reilly logo

Handbook of Automated Reasoning by Andrei Voronkov, Alan J.A. Robinson

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

3 Type systems for proof checking

As we see it, there is not one ‘right’ type system. The widely used theorem provers that are based on type theory all have inductive types. But then still there are other important parameters: the choice of allowed quantification and the choice of reduction relations to be used in the type conversion rule. We have already mentioned the possibility of allowing impredicative quantification or not. Also, we mentioned the β, δ, ι and η rules as possible reduction rules. A very powerful extension of the reduction relation is obtained by adding a fixed-point-operator Y:Π. A:Set.(A→A)→A satisfying

Y ƒ ( ) .

With this addition the reduction of the type system does not satisfy strong normalization ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required