Uniform and non uniform strategies for tableaux calculi for modal logics
作者:
Stéphane Demri,
期刊:
Journal of Applied Non-Classical Logics
(Taylor Available online 1995)
卷期:
Volume 5,
issue 1
页码: 77-96
ISSN:1166-3081
年代: 1995
DOI:10.1080/11663081.1995.10510844
出版商: Taylor & Francis Group
关键词: automated reasoning;modal logics;tableaux;strategies
数据来源: Taylor
摘要:
The major emphasis of this paper is on the definition of complete strategies in tableaux calculi for propositional modal logics. The strategies use a non exhaustive backtracking mechanism, a selective periodicity test and a uniform or a non uniform priority on the order of application of the tableaux rules. The propositional modal logics treated herein are those having a tableaux calculus with finite sets of formulas possibly occurring in the tableaux. Experimental results with the ATINF modal prover are presented.
点击下载:
PDF (1023KB)
返 回