First-Order Interpolation of Non-classical Logics Derived from Propositional Interpolation

被引：2
|
作者：
Baaz, Matthias [1 ]
Lolic, Anela [1 ]
机构：
[1] Tech Univ Wien, Inst Diskrete Math & Geometrie 104, Vienna, Austria
来源：
FRONTIERS OF COMBINING SYSTEMS (FROCOS 2017) | 2017年 / 10483卷
基金：
奥地利科学基金会;
关键词：
Proof theory; Interpolation; Lattice-based many-valued logics; Godel logics; INTUITIONISTIC LOGIC; GODEL LOGICS;
D O I：
10.1007/978-3-319-66167-4_15
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
This paper develops a general methodology to connect propositional and first-order interpolation. In fact, the existence of suitable skolemizations and of Herbrand expansions together with a propositional interpolant suffice to construct a first-order interpolant. This methodology is realized for lattice-based finitely-valued logics, the top element representing true and for (fragments of) infinitely-valued firstorder Godel logic, the logic of all linearly ordered constant domain Kripke frames.
引用
收藏
页码：265 / 280
页数：16
相关论文
共 50 条
12345