A Resolution-Based Theorem Prover for $${\textsf {K}}_{n}^{}$$Kn: Architecture, Refinements, Strategies and Experiments

Cláudia Nalon; Ullrich Hustadt; Clare Dixon

doi:10.1007/s10817-018-09503-x

A Resolution-Based Theorem Prover for $${\textsf {K}}_{n}^{}$$Kn: Architecture, Refinements, Strategies and Experiments

Cláudia Nalon, Ullrich Hustadt, Clare Dixon

Formal Methods

Research output: Contribution to journal › Article › peer-review

Abstract

In this paper we describe the implementation of , a resolution-based prover for the basic multimodal logic Kn. 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.

Original language	English
Journal	Journal of Automated Reasoning
DOIs	https://doi.org/10.1007/s10817-018-09503-x
Publication status	Published - 17 Mar 2020

Access to Document

10.1007/s10817-018-09503-x

Robotics and Artificial Intelligence for Nuclear (RAIN)
Lennox, B. (PI), Arvin, F. (CoI), Brown, G. (CoI), Carrasco Gomez, J. (CoI), Da Via, C. (CoI), Furber, S. (CoI), Luján, M. (CoI), Watson, S. (CoI), Watts, S. (CoI) & Weightman, A. (CoI)
2/10/17 → 31/03/22
Project: Research

Cite this

@article{d0056b5fa394467e9380994cc4907b6a,

title = "A Resolution-Based Theorem Prover for $${\textsf {K}}_{n}^{}$$Kn: Architecture, Refinements, Strategies and Experiments",

abstract = "In this paper we describe the implementation of , a resolution-based prover for the basic multimodal logic Kn. 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.",

author = "Cl{\'a}udia Nalon and Ullrich Hustadt and Clare Dixon",

year = "2020",

month = mar,

day = "17",

doi = "10.1007/s10817-018-09503-x",

language = "English",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Nature",

}

TY - JOUR

T1 - A Resolution-Based Theorem Prover for $${\textsf {K}}_{n}^{}$$Kn: Architecture, Refinements, Strategies and Experiments

AU - Nalon, Cláudia

AU - Hustadt, Ullrich

AU - Dixon, Clare

PY - 2020/3/17

Y1 - 2020/3/17

N2 - In this paper we describe the implementation of , a resolution-based prover for the basic multimodal logic Kn. 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.

AB - In this paper we describe the implementation of , a resolution-based prover for the basic multimodal logic Kn. 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.

U2 - 10.1007/s10817-018-09503-x

DO - 10.1007/s10817-018-09503-x

M3 - Article

SN - 0168-7433

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

ER -

A Resolution-Based Theorem Prover for $${\textsf {K}}_{n}^{}$$Kn: Architecture, Refinements, Strategies and Experiments

Abstract

Access to Document

Fingerprint

Projects

Robotics and Artificial Intelligence for Nuclear (RAIN)

Cite this