The Inference Rules

CADE-11 paper, 1992

Idea - Encode condensed detachment at the meta-level, for some rule

(provable(rule(A,C)) & provable(A)) => provable(C)
~provable(rule(A,C) | ~provable(A) | provable(C)

Idea - Provide known axioms at the meta-level

Idea - Use binary resolution to apply condensed detachment

Example - equivalential calculus

~provable(e(A,C)) | ~provable(A) | provable(C) #--CD
provable(e(e(X,Y),e(Y,X))) #--EC-4
provable(e(e(e(X,Y),Z),e(X,e(Y,Z)))) #--EC-5
~provable(e(e(e(a,v),e(c,a)),e(b,c))) #--Deny EC-1

Proof length measured by uses of CD

The Inference Rules

Overview

Set of Support

Unit and UR Resolution

Demodulation

Paramodulation

Condensed Detachment