On First-Order Model-Based Reasoning

TL;DR

This paper surveys various model-based reasoning methods in first-order logic, including resolution, tableaux, DPLL-inspired techniques, and introduces a new method called SGGS, emphasizing semantic guidance and recent advances.

Contribution

It provides a comprehensive overview of existing semantically-guided reasoning methods and introduces the novel SGGS approach for goal-sensitive reasoning in first-order logic.

Findings

Overview of resolution, tableaux, DPLL-inspired methods

Introduction of the SGGS method for first-order logic

Discussion of hierarchical, locality-based, and model-constructing methods

Abstract

Reasoning semantically in first-order logic is notoriously a challenge. This paper surveys a selection of semantically-guided or model-based methods that aim at meeting aspects of this challenge. For first-order logic we touch upon resolution-based methods, tableaux-based methods, DPLL-inspired methods, and we give a preview of a new method called SGGS, for Semantically-Guided Goal-Sensitive reasoning. For first-order theories we highlight hierarchical and locality-based methods, concluding with the recent Model-Constructing satisfiability calculus.