A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies
| Autor: | Marta Cialdea Mayer |
|---|---|
| Přispěvatelé: | Cialdea Mayer, Marta |
| Rok vydání: | 2019 |
| Předmět: |
Automated proof systems
Tableaux Modal logic Hybrid logic Programming language Computer science Modal logic 020207 software engineering 0102 computer and information sciences 02 engineering and technology Gas meter prover computer.software_genre Proof procedure 01 natural sciences Decidability TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics Fragment (logic) Description logic 010201 computation theory & mathematics Artificial Intelligence TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Hybrid logic computer Software Axiom |
| Zdroj: | Journal of Automated Reasoning. 64:135-165 |
| ISSN: | 1573-0670 0168-7433 |
| DOI: | 10.1007/s10817-019-09513-3 |
| Popis: | This work describes the Sibyl prover, an implementation of a tableau based proof procedure for multi-modal hybrid logic with the converse, graded and global modalities, and enriched with features largely used in description logics: transitivity and relation hierarchies. The proof procedure is provably terminating when the input problem belongs to an expressive decidable fragment of hybrid logic. After a description of the implemented proof procedure, the way how the implementation deals with the most delicate aspects of the calculus is explained. Some experimental results, run on sets of randomly generated problems as well as some hand-tailored ones, show only a moderate deterioration in the performances of the prover when the number of transitivity and inclusion axioms increase. Sibyl is compared with other provers (HTab, the hybrid logic prover whose expressive power is closer to Sibyl's one, and the first-order prover SPASS). The obtained results show that Sibyl has reasonable performances. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink