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

8.3 Equality elimination for the inverse method

Equality elimination for the inverse method is based on the same characterization of provability in terms of solution clauses as that for the tableau method (Theorem 8.6). However, the resulting calculi for the inverse method and for the tableau method are quite different because the inverse method is local while the tableaumethod is global. Among other inference rules, the inverse method uses the factoring rule that is absent in the tableau method. In a certain sense, equality elimination for tableaux and the inverse method are dual to each other which reflects the duality between bottom-up and top-down reasoning.

We will formulate the inverse method in the form of a logical calculus I ξ

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