A Graph Calculus for Predicate Logic

TL;DR

This paper presents a graph calculus method for classical first-order predicate logic that reduces logical consequence to graph emptiness, extending previous relation-based calculi.

Contribution

It introduces a novel refutation graph calculus for predicate logic, expanding on prior binary relation methods to handle more complex logical structures.

Findings

The calculus reduces logical validity to graph emptiness.

It converts graphs to normal form and expands them to detect contradictions.

The method effectively identifies unsatisfiable formulas in predicate logic.

Abstract

We introduce a refutation graph calculus for classical first-order predicate logic, which is an extension of previous ones for binary relations. One reduces logical consequence to establishing that a constructed graph has empty extension, i. e. it represents bottom. Our calculus establishes that a graph has empty extension by converting it to a normal form, which is expanded to other graphs until we can recognize conflicting situations (equivalent to a formula and its negation).