کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
10333720 689170 2016 20 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A bi-intuitionistic modal logic: Foundations and automation
ترجمه فارسی عنوان
یک منطق مداومی و بی منطقی: مبانی و اتوماسیون
کلمات کلیدی
منطق شهودی، منطق مودال، سیستم تابلو فرش، تصمیم گیری، قضیه مکاتبات،
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی
The paper introduces a bi-intuitionistic modal logic, called BISKT, with two adjoint pairs of tense operators. The semantics of BISKT is defined using Kripke models in which the set of worlds carries a pre-order relation as well as an accessibility relation, and the two relations are linked by a stability condition. A special case of these models arises from graphs in which the worlds are interpreted as nodes and edges of graphs, and formulae represent subgraphs. The pre-order is the incidence structure of the graphs. We present a comprehensive study of the logic, giving decidability, complexity and correspondence results. We also show the logic has the effective finite model property. We present a sound, complete and terminating tableau calculus for the logic and use the MetTeL system to explore implementations of different versions of the calculus. An experimental evaluation gave good results for satisfiable problems using predecessor blocking.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 85, Issue 4, June 2016, Pages 500-519
نویسندگان
, , ,