HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)

We present HYPNO (HYpersequent Prover for NOn-normal modal logics), a Prolog-based theorem prover and countermodel generator for non-normal modal logics. HYPNO implements some hypersequent calculi recently introduced for the basic system [Formula: see text] and its extensions with axioms M, N, and C...

Descripción completa

Detalles Bibliográficos
Autores principales: Dalmonte, Tiziano, Olivetti, Nicola, Pozzato, Gian Luca
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324037/
http://dx.doi.org/10.1007/978-3-030-51054-1_23
_version_ 1783551868401614848
author Dalmonte, Tiziano
Olivetti, Nicola
Pozzato, Gian Luca
author_facet Dalmonte, Tiziano
Olivetti, Nicola
Pozzato, Gian Luca
author_sort Dalmonte, Tiziano
collection PubMed
description We present HYPNO (HYpersequent Prover for NOn-normal modal logics), a Prolog-based theorem prover and countermodel generator for non-normal modal logics. HYPNO implements some hypersequent calculi recently introduced for the basic system [Formula: see text] and its extensions with axioms M, N, and C. It is inspired by the methodology of [Image: see text], so that it does not make use of any ad-hoc control mechanism. Given a formula, HYPNO provides either a proof in the calculus or a countermodel, directly built from an open saturated hypersequent. Preliminary experimental results show that the performances of HYPNO are very promising with respect to other theorem provers for the same class of logics.
format Online
Article
Text
id pubmed-7324037
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73240372020-06-30 HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description) Dalmonte, Tiziano Olivetti, Nicola Pozzato, Gian Luca Automated Reasoning Article We present HYPNO (HYpersequent Prover for NOn-normal modal logics), a Prolog-based theorem prover and countermodel generator for non-normal modal logics. HYPNO implements some hypersequent calculi recently introduced for the basic system [Formula: see text] and its extensions with axioms M, N, and C. It is inspired by the methodology of [Image: see text], so that it does not make use of any ad-hoc control mechanism. Given a formula, HYPNO provides either a proof in the calculus or a countermodel, directly built from an open saturated hypersequent. Preliminary experimental results show that the performances of HYPNO are very promising with respect to other theorem provers for the same class of logics. 2020-06-06 /pmc/articles/PMC7324037/ http://dx.doi.org/10.1007/978-3-030-51054-1_23 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Dalmonte, Tiziano
Olivetti, Nicola
Pozzato, Gian Luca
HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
title HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
title_full HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
title_fullStr HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
title_full_unstemmed HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
title_short HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
title_sort hypno: theorem proving with hypersequent calculi for non-normal modal logics (system description)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324037/
http://dx.doi.org/10.1007/978-3-030-51054-1_23
work_keys_str_mv AT dalmontetiziano hypnotheoremprovingwithhypersequentcalculifornonnormalmodallogicssystemdescription
AT olivettinicola hypnotheoremprovingwithhypersequentcalculifornonnormalmodallogicssystemdescription
AT pozzatogianluca hypnotheoremprovingwithhypersequentcalculifornonnormalmodallogicssystemdescription

Ejemplares similares