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 ξ
Get Handbook of Automated Reasoning now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
