On First-Order Model-Based Reasoning
This is an incremental survey paper for researchers in automated reasoning and logic.
The paper surveys model-based reasoning methods for first-order logic, addressing the challenge of semantic reasoning, and previews a new method called SGGS.
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.