On First-Order Model-Based Reasoning
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.
Cite
@article{arxiv.1502.02535,
title = {On First-Order Model-Based Reasoning},
author = {Maria Paola Bonacina and Ulrich Furbach and Viorica Sofronie-Stokkermans},
journal= {arXiv preprint arXiv:1502.02535},
year = {2019}
}
Comments
In Narciso Marti-Oliet, Peter Olveczky, and Carolyn Talcott (Eds.), "Logic, Rewriting, and Concurrency: Essays in Honor of Jose Meseguer" Springer, Lecture Notes in Computer Science 9200, September 2015, 24 pages. Version v4 in arxiv fixes a typo on page 15 that remains in the version published in the Springer book