Basing Sequent Systems on Exclusive-Or

被引：0
|
作者：
Avron, Arnon [1 ]
机构：
[1] Tel Aviv Univ, Sch Comp Sci, IL-69978 Tel Aviv, Israel
来源：
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2021 | 2021年 / 12842卷
基金：
以色列科学基金会;
关键词：
Analytic Gentzen-type proof systems; Cut-elimination; Translations; Hypersequents;
D O I：
10.1007/978-3-030-86059-2_7
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
In the standard Gentzen-type systems for classical logic, the right hand side of a sequent is interpreted as the inclusive-or of its elements. In this paper we investigate what happens if the exclusive-or. is used instead. We provide corresponding analytic systems, and some of the decision procedures that are based on them. The latter are particularly efficient for the negation-equivalence fragment of classical logic.
引用
收藏
页码：112 / 128
页数：17
相关论文
共 50 条
12345