Back to Search
Start Over
A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments.
- Source :
- Journal of Automated Reasoning; Mar2020, Vol. 64 Issue 3, p461-484, 24p
- Publication Year :
- 2020
-
Abstract
- In this paper we describe the implementation of , a resolution-based prover for the basic multimodal logic K n . The prover implements a resolution-based calculus for both local and global reasoning. The user can choose different normal forms, refinements of the basic resolution calculus, and strategies. We describe these options in detail and discuss their implications. We provide experiments comparing some of these options and comparing the prover with other provers for this logic. [ABSTRACT FROM AUTHOR]
- Subjects :
- CALCULUS
MATHEMATICS
LOGIC
FREE resolutions (Algebra)
Subjects
Details
- Language :
- English
- ISSN :
- 01687433
- Volume :
- 64
- Issue :
- 3
- Database :
- Complementary Index
- Journal :
- Journal of Automated Reasoning
- Publication Type :
- Academic Journal
- Accession number :
- 142000137
- Full Text :
- https://doi.org/10.1007/s10817-018-09503-x