Semantic Incompleteness of Hilbert System for a Combination of Classical and Intuitionistic Propositional Logic
本文证明del Cerro和Herzig提出的希尔伯特系统(C+J)−因缺少经典肯定前件规则而在语义上不完备，并利用Priest的悖论逻辑给出论证。
2023-12-26 cs.LO
On a Partial Decision Method for Dynamic Proofs
本文讨论了自适应逻辑ACLuN1的命题片段的目标导向证明过程。在命题层次上，它形成了一个最终可导性的算法。如果扩展到谓词层面，它提供了一个标准的最后推导。鉴于缺乏阳性检测，这一点至关重要。这个过程可以推广到所有的平坦自适应逻辑。
2002-07-25 cs.LO
LPC(ID): A Sequent Calculus Proof System for Propositional Logic Extended with Inductive Definitions
Carnegie Mellon University（卡内基梅隆大学）；Katholieke Universiteit Leuven（鲁汶大学）
逻辑FO（ID）使用来自逻辑编程领域的思想来扩展具有非单调归纳定义的一阶逻辑。这种逻辑形式上扩展了逻辑程序设计、溯因逻辑程序设计和数据逻辑，从而将对这些形式主义的看法形式化为（广义）归纳定义的逻辑。本文的目标是研究FO（ID）的命题片段PC（ID）的演绎推理方法。我们引入了一个正式的证明系统的基础上的演算（根森式演绎系统），这种逻辑。由于PC（ID）是经典命题逻辑和命题归纳定义的集成，我们的推理演算证明系统集成了命题演算和定义的推理规则。我们提出了这个证明系统的可靠性和完整性，相对于PC（ID）的一个略有限制的片段。我们还提供了PC（ID）的一些复杂性结果。通过对PC（ID）证明系统的开发，有助于加深对FO（ID）证明理论基础的理解，从而研究FO（ID）的有效证明系统。
2012-07-11 cs.AI cs.LO
A propositional system induced by Japaridze's approach to IF logic
循环演算（英语：Cirquent calculus）是G.Japaridze为了满足可计算逻辑的需要而提出的一种新的证明理论和语义方法，他还表明，通过循环演算，人们可以捕获，提炼和推广独立友好（IF）逻辑。具体来说，这种方法允许我们考虑独立于命题连接词的精神，就像传统的IF逻辑考虑独立于量词一样。雅帕里泽的治疗IF逻辑，但是，是纯粹的语义，并没有演绎系统提出。本文构造了一个完备的形式系统。Japaridze的基于循环的IF逻辑语义的命题片段。这样一个系统因此可以被认为是一个公理化的纯命题IF逻辑在其充分的一般性。
2014-05-23 cs.LO math.LO
A Decidable Timeout based Extension of Propositional Linear Temporal Logic
我们开发了一个基于超时的命题线性时序逻辑扩展（我们称之为TLTL），用于指定基于超时的实时的系统模型的时序特性。TLTL公式明确引用了一个运行的全局时钟以及静态定时变量和一个抽象超时行为的动态变量。我们扩展LTL的能力，表示超时约束。从表现力的观点来看，TLTL不能与包括TPTL、XCTL和MTL的重要的已知的基于时钟的实时逻辑相比，即，TLTL可以指定某些属性，这些属性不能在这些逻辑中指定（反之亦然）。我们定义了一个相应的超时表TLTL公式的可满足性检查。提出了一种基于超时Kripke结构的模型检验算法。此外，我们证明了这种扩展逻辑的有效性检查仍然是PSPACE完全的，即使在存在超时约束和无限状态模型。在离散时间语义下，有界的超时增量，模型检查问题，如果一个TLTL公式成立的超时Kripke结构也是PSPACE完全的。我们进一步证明了当TLTL在离散时间上解释时，它可以嵌入到一元二阶逻辑中，而当TLTL在稠密时间上解释而不满足非顶点条件时，所得到的逻辑是$Σ_1^1$ -完全的.
2010-12-16 cs.LO
Set theory and tableaux for teaching propositional logic
在这项工作中，我们建议使用一套理论的解释语义tableaux教学命题逻辑。如果学生以前有基本集合论的概念，这种语义表的方法可以澄清她的语义树的操作方式，连接过程的语法和语义方面。此外，它可能有助于介绍逻辑中更高级的主题，如模态逻辑。
2015-07-14 cs.CY cs.LO
Towards Non-Monotonic Entailment in Propositional Defeasible Standpoint Logic
University of Cape Town and CAIR, South Africa（开普敦大学和CAIR，南非）；Université Sorbonne Paris Nord, Inserm, Sorbonne Université, Limics, 93017 Bobigny, France（巴黎-索邦大学，Inserm，索邦大学，Limics，法国93017博比尼）；ISTI-CNR, Pisa, Italy（意大利比萨ISTI-CNR）
本文通过引入情境立场条件句，将KLM风格的非单调理性蕴涵关系提升到命题可废止立场逻辑（PDSL）的一个片段中，并证明了该片段可表达为一组情境条件句，进而将基于排序的蕴涵关系（如理性和词典序闭包）从命题情况忠实翻译到PDSL，同时保持复杂度界限。
2026-06-02 cs.AI cs.LO
Generalizing Redundancy in Propositional Logic: Foundations and Hitting Sets Duality
University College Dublin（都柏林大学学院）；IST/INESC-ID（里斯本高等理工学院/葡萄牙国家系统与计算机工程研究所）
从合取范式（CNF）中的命题公式中检测和消除冗余子句是包括人工智能在内的许多应用领域的基本问题，并且已经成为广泛研究的主题。此外，一些最近的应用程序激发了这个问题的各种扩展。例如，不可满足的公式划分为不相交的子句子集（所谓的组），通常需要通过删除冗余组来简化，或者可能包含冗余变量，而不是子句。在这份报告中，我们提出了一个广义的理论框架标记CNF公式，统一的冗余检测和删除问题的各种扩展，并允许推导出一些结果，substanion和扩展以前的工作。后续报告包含了一些额外的理论结果和算法的各种计算问题的背景下，提出的框架。
2012-07-10 cs.AI cs.LO
Algebraic Semantics for Relative Truth, Awareness, and Possibility
本文提出了一类代数结构，相对化布尔代数（RBAs），提供命题逻辑中的真/有效性只定义相对于一个局部域的语义。特别是，事件及其补集的连接不需要是顶部元素。尽管如此，行为是由命题逻辑定律局部支配的。通过进一步赋予这些结构以算子-类似于模态代数的理论-RBA充当模态逻辑的模型，其中真理是相对的。特别是，模态RBAs提供了各种众所周知的感知逻辑的语义和可能性语义的另一种观点。
2021-10-05 cs.LO
Enumeration Complexity of Poor Man's Propositional Dependence Logic
依赖逻辑（英语：Dependence logics）是一个现代的独立和依赖逻辑家族，模仿数据库理论的概念。本文旨在开创依赖逻辑领域中枚举复杂性的研究，从而对数据库查询答案的枚举问题提出一个新的观点。因此，作为第一步，我们调查的问题，枚举所有满足队的公式从一个给定的片段命题依赖逻辑。我们区分由任意函数限制团队规模和参数化版本，其中参数是团队规模。我们表明，多项式延迟可以达到多项式，否则在参数化设置，我们达到FPT延迟。然而，构造的具有多项式延迟的枚举算法需要指数空间。我们证明了一个增量多项式延迟算法存在，它只使用多项式空间。相反，我们表明，对于一般的问题，没有限制的团队规模，在多项式空间中运行的枚举算法不存在。
2018-03-12 cs.CC cs.LO
An Analytic Propositional Proof System on Graphs
本文提出一种直接作用于任意无向图的解析证明系统，利用模块分解和深度推理技术，证明了切割容许性与分裂性质推广，并表明其为带混合的乘法线性逻辑的保守扩展，图被视为广义联结词。
2022-10-20 cs.LO
Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic
证明理论语义学（Proof-theoretical Semantics，P-tS）是一种语义学范式，其中逻辑中的意义基于证明（而不是真理）。直觉命题逻辑（IPL）的P-tS的一个特殊实例是它的基扩展语义（B-eS）。这种语义由一个称为支持的关系给出，解释逻辑常数的含义，它由称为基础的规则系统参数化，提供原子命题的语义。在本文中，我们解释的基础上收集的明确的公式，并使用统一的证明搜索-逻辑编程（LP）的证明理论的基础-提供后者的操作视图-建立完整的IPL的B-eS。这种观点允许否定，P-tS中的一个微妙的问题，被理解为在LP中的否定失败协议。具体地说，虽然对命题的否定在传统上被理解为对命题否定的断言，但在B-eS中，我们可以将对命题的否定理解为未能找到对命题的证明，这样，断言和否定都是P-tS中的基本概念。
2023-03-28 cs.LO math.LO
Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
IBM Research -- Tokyo（IBM研究院（东京））；Kyoto University（京都大学）
受深度神经网络（DNN）在机器学习中的最新发展的启发，我们探索了它们在PL相关主题中的应用。本文是实现这一目标的第一步;我们提出了一种无否定命题逻辑的证明合成方法，其中我们使用DNN来获得证明搜索的指南。这个想法是把证明综合问题看作是从命题到其证明的转换。我们训练seq 2seq，这是神经机器翻译中的一个流行网络，因此它生成一个编码为给定命题的$λ$ -项的证明。我们实现了整个框架，并根据经验观察到，生成的证明项在AST的树编辑距离方面接近于正确的证明。这一观察结果证明了使用经过训练的seq 2seq模型的输出作为证据搜索的指导是合理的。
2017-06-20 cs.AI cs.LO cs.PL
On an ecumenical natural deduction with stoup -- Part I: The propositional case
由Gentzen提出并由Prawitz进一步研究的自然演绎系统是最著名的证明理论框架之一。它的成功部分是基于这样一个事实，即自然演绎规则呈现了逻辑常数的简单表征，特别是在直觉主义逻辑的情况下。然而，为了处理经典逻辑而对直觉规则集进行扩展的做法受到了很多批评。事实上，大多数这样的扩展都在通常的引入和消除规则之外增加了管理否定的额外规则。因此，几个元逻辑属性，最突出的一个是和谐，失去了。Dag Prawitz提出了一个自然演绎的普世体系，其中经典逻辑和直觉主义逻辑被编入同一个体系。在这个系统中，古典主义逻辑学家和直觉主义逻辑学家将共享全称量词、合取词、否定词和荒谬的常量，但他们各自有自己的存在量词、析取词和蕴涵词，具有不同的含义。Prawitz的主要观点是，这些不同的含义是由一个双方都能接受的语义框架给出的。在本文中，我们提出了一种不同的方法适应，自然演绎框架，吉拉德的stoup机制。这将允许定义一个纯粹的和谐自然演绎系统的命题片段普拉维茨的普世逻辑。
2022-04-06 cs.LO
Propositional Dynamic Logic for Hyperproperties
反应式系统的信息安全属性（如非干扰性）通常需要将系统的不同执行相互关联并同时遵循它们。这样的超性质在其他上下文中也可以是有用的，例如，当分析分布式系统的属性时，如线性化。由于LTL、CTL或模态μ演算等常见逻辑无法表达超性质，因此开发了超逻辑HyperLTL和HyperCTL* 来解决这个缺陷。然而，这些逻辑不能表达任意的Ω-正则性质。在本文中，我们介绍HyperPDL-三角洲，一个适应的命题动态逻辑的Fischer和Ladner的hyperproperties，为了消除这一限制。使用一个优雅的自动机理论框架，我们表明，HyperPDL-三角洲模型检验是渐近不更昂贵的HyperCTL* 模型检验，尽管它大大增加了表达能力。我们进一步研究片段的HyperPDL-三角洲方面的可满足性检查。
2020-07-17 cs.FL cs.LO
Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas
Sun Yat-sen University（中山大学）
\emph{Canonical (logic) programs}（CP）是指用连接符$not\ not$扩充的正常逻辑程序。在本文中，我们解决的问题，是否CP是\emph{succinctly incomparable}与\emph{propositional formulas}（PF）。我们的主要结果表明，奇偶性问题，它可以多项式表示在PF，但\emph{only}有指数表示在CP。换句话说，来自CP的PARITY \emph{separates} PF。简单地说，这意味着当将PF中的一组公式转换为CP中的等效程序时（不引入新变量），指数大小的爆破通常是不可避免的。此外，由于Lifschitz和Razborov已经表明，将CP与PF分开也存在问题（假设$\mathsf{P}\nsubseteq \mathsf{NC^1/poly}$），因此CP和PF确实是不可比较的。从计算理论的观点来看，上述结果也可以被认为是两个\emph{models of computation}的分离，即，我们在$\mathsf{NC^1/poly}$中识别出一种语言，该语言不在多项式大小的CP程序可计算的语言集合中。
2015-01-24 cs.AI cs.LO
Prime Implicates and Prime Implicants: From Propositional to Modal Logic
University of Bremen（不来梅大学）
素蕴涵和素蕴涵已经被证明与人工智能的许多领域相关，最显著的是溯因推理和知识编译。本文的目的是研究如何将这些概念从命题逻辑适当地扩展到模态逻辑K。我们在论文的开头考虑了K的子句和术语的一些可能的定义。不同的定义进行评估方面的一组句法，语义和复杂性理论的性质特征的命题定义。然后，我们比较的定义方面的性质的概念，他们诱导的素蕴涵和素蕴涵。虽然没有定义，完美地概括了命题的概念，我们表明，确实存在一个定义，满足许多理想的性质的命题的情况下。在论文的后半部分，我们考虑了所选定义的计算性质。为此，我们提供了健全的和完整的算法生成和识别总理牵连，我们表明总理牵连识别任务是PSPACE完成。我们还证明了上界和下界的大小和数量的素数蕴涵。虽然本文的重点是逻辑K，我们所有的结果同样适用于多模态K和描述逻辑ALC中的概念表达式。
2014-01-15 cs.AI cs.LO
A cirquent calculus system with clustering and ranking
循环演算是G.Japaridze为了满足其可计算逻辑理论的需要而提出的一种新的证明理论和语义方法。Japaridze的早期文章“From formulas to cirquents in computability logic”将cirquents的概念推广到了所谓的聚类和排序的版本，并表明，通过聚类和排序的cirquents，可以捕获，提炼和推广所谓的扩展IF逻辑。雅帕里泽的治疗扩展IF逻辑，但是，是纯粹的语义，并没有演绎系统提出。本文从句法上构造了一个具有聚类和排序功能的、可靠的、完备的w.r.t.基于情境的语义学的命题片段。这样一个系统不仅可以被认为是经典命题逻辑的保守扩展，而且当被限制为不超过2秩的cirquents时，也可以被认为是完全一般性的纯命题扩展IF逻辑的公理化。
2014-09-11 cs.LO
The Computational Complexity of Propositional Cirquent Calculus
在2006年由Japaridze提出，cirquent演算是一个改进的cirquent演算。由于需要一个具有更明确的资源推理能力的演绎系统，因此出现了cirquent演算。与操纵树状对象（公式、序列等）的更传统的证明理论方法不同，cirquent演算基于称为cirquent的电路风格结构，其中不同的“对等体”（兄弟姐妹，表亲等）子结构可以共享组件。正是这种资源共享机制，使Cirquent演算具有了新颖性（和优点）。从一开始，cirquent演算就与抽象的资源语义配对。这种语义允许对资源提供者和资源用户之间的交互进行推理，其中资源以其最一般和直观的意义被理解。在一个更有限的计算意义上解释资源已经取得了cirquent演算工具公理化的各种基本片段的可计算性逻辑，一个正式的理论（互动）可计算性。在没有特别麻烦的收缩规则的情况下，所谓的“经典”的Cirquent演算规则产生了一个健全而完整的可计算性逻辑系统CL 5。本文研究了CL 5的计算复杂性，证明了它是$Σ_2^p$ -完全的.我们还表明，CL 5没有重复规则的多项式大小的证明，是NP-完全的。
2015-03-24 cs.LO
An Abstract Algebraic Logic View on Judgment Aggregation
在本文中，我们提出了抽象代数逻辑（AAL）作为一般的逻辑框架的判断聚合。我们的主要贡献是一个广义的赫茨伯格的代数方法来表征的结果在判断聚合和命题态度聚合，表征某些Arrovian类聚合布尔代数和MV-代数同态，分别。本文的刻画结果适用于任意自延逻辑的公式议程。这个概念来自AAL，包含了大量的逻辑，其中经典逻辑、直觉逻辑、模态逻辑、多值逻辑和关联逻辑都是特例。AAL的一般理论将一类唯一的代数$\Alg\Sm$规范地关联到每个自扩张逻辑$\Sm$。我们表明，对于任何自扩展逻辑$\Sm$，使$\Alg\Sm$是封闭的直积下，任何代数$\Alg\Sm$可以采取的真值集上的聚合问题可以制定。通过这种方式，在经典，直觉，模态，多值和相关逻辑形式化的议程上的判断聚合可以被统一地捕获为特例。这为系统研究由复杂公式组成的广泛的“现实议程”铺平了道路，这些公式的命题连接词的解释方式偏离了它们的经典解释。正如迪特里希所观察到的，这一点特别有趣，因为逻辑连接词的非经典（虚拟）解释可以提供一种逃避不可能结果的策略。
2016-03-27 cs.LO
Interpolation for Converse PDL
本文证明Converse PDL具有局部Craig插值性质及Beth可定义性，通过改编Maehara方法并引入带分析性切割规则和焦点机制的循环矢列系统完成证明。
2025-09-17 cs.LO
Defining Logical Systems via Algebraic Constraints on Proofs
本文提出利用约束代数将非经典逻辑证明系统分解为更简单逻辑（如经典逻辑）的证明系统，实现统一模块化的证明理论处理，并搭建语义与证明理论的桥梁。
2023-10-19 cs.LO math.LO
Proof-theoretic Semantics for First-order Logic
本文为一阶经典逻辑的证明论语义提供了一种初等、构造性且原生的完备性证明，并同时给出一阶直觉主义逻辑的可靠性与完备性证明。
2025-07-17 cs.LO math.LO
Proof-graphs for Minimal Implicational Logic
众所周知，命题经典证明的规模可能是巨大的。证明理论研究发现正常或切割自由证明和他们各自的非正常证明之间的指数差距。本文的目的是研究如何降低命题推理的权重。我们提出了形式主义的证明图的纯蕴涵逻辑，这是一个特定的形状，旨在捕捉演绎的逻辑结构的图形。这种形式主义的优点是公式可以在简化证明中共享。本文给出了最小蕴涵逻辑证明图的精确定义，并给出了证明图的规范化过程。与标准的树状形式主义相比，我们的规范化并没有增加节点的数量，当应用到相应的最小证明图表示。
2014-04-01 cs.LO
Categorical Proof-Theoretic Semantics
本研究将Sandqvist的直觉主义命题逻辑基扩展语义与预层范畴证明论关联，从范畴论重构可靠性与完全性论证，证明其构造的自然性，并指出该语义可视为层范畴中的自然析取。
2024-02-01 cs.LO math.CT math.LO
Category theoretic semantics for theorem proving in logic programming: embracing the laxness
命题逻辑程序$P$可以用程序中的原子命题集合上的$P_fP_f$ -余代数来标识。相应的$C(P_fP_f)$ -余代数，其中$C(P_fP_f)$是$P_fP_f$上的余自由余代数，描述了归结导子.使用宽松的语义，这种对应关系可以扩展到一类没有存在变量的一阶逻辑程序。由此产生的扩展捕获逻辑编程中的术语匹配分辨率的证明。完善宽松的方法，我们进一步扩展到任意逻辑程序。我们还展示了一个完善的Bonchi和Zanasi的饱和语义逻辑编程，补充宽松的语义。
2016-02-17 cs.LO
On optimal heuristic randomized semidecision procedures, with application to proof complexity
（p-）最优命题证明系统的存在性是（证明）复杂性中的一个主要公开问题;许多人猜测这样的系统不存在。Krajicek和Pudlak（1989）证明了这个问题等价于存在一个算法，这个算法在所有的命题重言式上都是最优的。Monroe（2009）最近给出了一个猜想，暗示这样的算法不存在。我们表明，在错误的存在下，这样的最佳算法确实存在。这个概念的动机是启发式算法的概念。也就是说，我们允许算法声称少量的假“定理”（根据任何采样分布的非重言式）和错误的有界概率在其他输入。我们的结果也可以被看作是存在的最佳证明系统在一类证明系统通过推广自动化证明系统。
2010-02-03 cs.CC cs.LO
Exploring the bidimensional space: A dynamic logic point of view
我们提出了一个家庭的逻辑推理代理的位置和运动在平面上有几个潜在的应用领域的多智能体系统（MAS），如多智能体规划和机器人。最一般的逻辑包括（i）原子公式，用于表示给定事实的真实性或给定代理在平面的某个位置的存在，（ii）原子程序，对应于平面中的四个基本方向（上，下，左，右）以及命题动态逻辑的四个程序构造（顺序组合，非确定性组合，迭代和测试）。由于这种逻辑是不可计算的，我们研究了它的一些有趣的可判定和可公理化的片段，并给出了一个可判定的扩展，它的无迭代片段通过表示智能体在平面上运动的特殊程序来实现。
2017-02-06 cs.AI cs.LO
Standpoint Logics with Defeasible Beliefs
University of Cape Town（开普敦大学）；CAIR, South Africa（南非人工智能研究中心）；Technische Universität Dresden（德累斯顿工业大学）；ScaDS.AI – Center for Scalable Data Analytics and Artificial Intelligence Dresden/Leipzig, Germany（德国德累斯顿/莱比锡可扩展数据分析与人工智能中心）
将KLM可废止逻辑与立场逻辑框架结合，提出DRSL，通过公理化语义和多种蕴涵关系提升，实现多视角下可废止信念的形式化表达。
2026-06-07 cs.AI cs.LO
A syntactic proof of decidability for the logic of bunched implication BI
本文通过证明论方法，给出了bunched implication逻辑BI可判定性的语法证明，提供了可实现的决策程序并界定了逻辑复杂性。
2026-01-03 cs.LO
Lower Bounds on Inverse Cellular Automata via Proof Complexity
Charles University（查理大学）
研究有限大小配置上逆细胞自动机的复杂性，通过将UNSAT归约到该问题简化证明其co-NP完全性，并展示其在弱算术理论V^0中可形式化，利用已知的受限深度Frege系统下界和Paris-Wilkie翻译，得出逆细胞自动机大小的下界。
2026-04-01 cs.DM cs.LO math.LO
Proving Infinitary Formulas
这里和那里的无穷命题逻辑由于与逻辑程序的强等价变换的关系而对回答集程序设计理论有重要意义。我们知道存在一个公理化这个逻辑的形式系统，但是在这个系统中的一个证明可能包括无限多个公式。本文描述了Here-There逻辑中无穷公式的有效性与某些有限演绎系统中公式的可证性之间的关系。这种关系允许我们使用有限证明来证明无穷公式的有效性。这篇笔记正在考虑发表在《逻辑程序设计的理论与实践》上。
2016-08-04 cs.LO
An analytic calculus for intuitionistic belief
直觉主义信念已经被阿特莫夫（Artemov）和普罗托波佩斯库（Protopescu）公理化为直觉主义命题逻辑的扩展，通过分配方案K和共反射$A\rightarrow\Box A$。通过这种方式，信念被解释为验证的结果，并且它适合于具有认知模态的直觉主义命题逻辑的扩展的Brouwer-Heyting-Kolmogorov解释。本文研究了直觉信念的自然演绎系统$\mathsf{IEL}^{-}$的结构性质。重点讨论了微积分的解析性，首先证明了正规化定理和子公式性质。从这些，逻辑的可判定性和一致性遵循作为推论。最后，用纯证明论的方法建立了析取性质、$\Box$ -素性和反射规则的可容许性。
2021-06-27 cs.LO math.LO
Mechanised uniform interpolation for modal logics K, GL, and iSL
本文在 Coq 中机械化计算并证明了模态逻辑 K、GL 和 iSL 的命题量词可定义性（一致插值），完善了 GL 的现有证明，实现了 iSL 的首次证明论构造，并提供了经过验证的计算程序。
2024-04-29 cs.LO math.LO
A proof-theoretic approach to uniform interpolation property of multi-agent modal logic
针对多智能体模态逻辑缺乏证明论进路UIP证明的问题，本文扩展已有证明系统，提出纯句法算法，证明了$\boldsymbol{\text{K}_n}$等三类多智能体模态逻辑的一致插值性质，还给出了无需二阶量词的直接证明。
2025-10-29 cs.LO
On Expansion and Resolution in CEGAR Based QBF Solving
量化布尔公式（QBF）是一个用泛量化和存在量化在命题上扩展的命题公式。基于CEGAR的QBF求解技术有两种方法，一种是基于建立部分扩展的精化循环，另一种是基于满足子句的通信。尽管它们的算法相似，但它们在实验评估中的性能特征非常不同，并且在许多情况下是正交的。我们比较这些CEGAR方法使用证明理论开发的QBF解决方案，并提出了一个统一的演算，结合了这两种方法的力量。最后，我们实现了新的演算，并通过实验证实，理论上的改进导致性能的提高。
2018-03-26 cs.LO
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
本文首次探索子结构逻辑的证明论语义，提出直觉主义乘法线性逻辑（IMLL）的基础扩展语义，其中逻辑常量定义均采用消去规则形式，并证明了其可靠性与完备性。
2024-11-12 cs.LO math.LO
Wijesekera-style constructive modal logics
我们定义了一个命题构造性模态逻辑族，每个模态逻辑对应于一个不同的经典模态系统。逻辑定义在风格的Wijesekera的建设性模态逻辑，并证明理论和语义动机。一方面，它们对应于经典模态逻辑的标准演算的单一后继限制。另一方面，它们是通过将直觉Kripke模型的遗传性纳入模态公式的经典满足子句而获得的。我们表明，对于所考虑的经典逻辑，证明理论和语义方法返回相同的建设性系统。
2022-10-18 cs.LO math.LO
Base-extension Semantics for Modal Logic
本文为经典命题模态系统 K、KT、K4 和 S4 开发了基扩展语义，以 $\square$ 为主算子，建立了可靠性与完备性定理及 $\square$ 与 $\lozenge$ 的对偶性，并指出该语义对欧几里得模态逻辑不完备。
2024-02-12 cs.LO math.LO
The naturality of natural deduction (II). Some remarks on atomic polymorphism
在以前的文件（这是一个起诉），我们研究了提取的证明理论性质的自然演绎推导从他们的非谓词翻译到系统F。我们的主要思想是引入一个扩展的方程理论系统F编纂在语法层面上的一些参数模型中发现的属性。在最近的一系列论文中，提出了一种不同的方法来提取自然演绎推导的证明论性质，方法是定义通常翻译的谓词变体，将直觉命题逻辑嵌入系统F的原子片段。在本文中，我们表明，这种方法找到了一个一般的解释，在我们的方程研究的二阶自然演绎，并提供了一个明确的语义理由参数。
2021-01-04 cs.LO math.LO
Proust: A Nano Proof Assistant
Proust是一个小Racket程序，为命题和谓词逻辑的验证证明的开发提供基本的交互式帮助。它是分阶段构建的，其中一些是由学生在使用它来完成证明练习之前完成的，并且与其理论基础的研究平行，包括马丁-洛夫类型论的元素。目标是双重的：揭开Coq和Agda等全功能证明助手背后的一些机制的神秘面纱，并更好地将形式逻辑的研究与本科计算机科学课程的其他核心要素结合起来。
2016-11-29 cs.LO cs.PL
Complexity Results in Team Semantics: Nonemptiness Is Not So Complex
University of Helsinki（赫尔辛基大学）；Utrecht University（乌得勒支大学）
研究团队语义中凸逻辑的复杂性，针对带非空原子NE的经典命题逻辑扩展，证明可满足性问题是NP完全的，有效问题是coNP完全的，模型检验问题属于P。
2026-02-26 cs.LO math.LO
Game-theoretic Interpretation of Type Theory Part II: Uniqueness of Identity Proofs and Univalence
在本文中，基于以前的工作（第一部分），我们提出了一个游戏语义的内涵变体的直觉类型论，反驳了唯一性的原则，身份证明和验证的univalence公理，虽然我们不解释非平凡的高等命题等式。具体来说，根据霍夫曼和Streicher的历史广群解释，我们配备了一个广群结构的第一部分中的谓词游戏，这引起了（谓词）gamoid的概念。粗略地说，gamoids是“指定（计算）等式的游戏”，它解释了ID类型中的微妙之处。然后，我们制定了一个类别的家庭的预测gamoid，配备了依赖产品，依赖和，ID类型以及宇宙，这形成了一个具体的实例的广群模型。我们相信，这项工作是一个重要的垫脚石走向一个完整的解释同伦类型论。
2016-04-05 cs.LO math.CO math.CT
A Subatomic Proof System for Decision Trees
我们设计了一个证明系统的命题经典逻辑，集成了两种语言的布尔函数：标准的合取-析取-否定和二进制决策树。我们给出了两个这样做的理由。第一个是证明理论的自然性：该系统由最近引入的亚原子逻辑的单一，简单，线性方案产生的所有推理规则组成。由于这种规律性，通过自然的结构消除了切口。第二个原因是系统生成有效的证明。事实上，我们表明，由于Statman，这不能有更好的比指数切割免费证明在微积分的重言式的某一类，有多项式切割免费证明在我们的系统。我们通过使用与切消元相同的结构来实现这一点。总之，通过扩展命题逻辑的语言，我们使其证明理论更加规则，并生成更多的证明，其中一些是非常有效的。这种设计是通过将原子视为其真值的叠加而实现的，这些真值由自对偶、非交换连接词连接。然后，一个证明可以通过每个原子投影成两个证明，每个真值一个，而不需要切割。这些投射在语义上是自然的，是本文结构的核心。为了适应自对偶的非交换性，我们在深度推理中组合证明。
2022-06-30 cs.LO math.LO
Base-extension Semantics for Intuitionistic Modal Logics
本文为Simpson直觉主义模态逻辑建立基扩展语义，并证明其相对自然演绎系统的可靠性与完备性。
2025-07-09 cs.LO math.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
Object-Level Reasoning with Logics Encoded in HOL Light
我们提出了一个通用的框架，有利于对象级推理与逻辑编码的高阶逻辑定理证明环境HOL光。这涉及到在任何逻辑中使用直观的前向和后向链接以微积分风格证明语句。它是由自动化的机器，照顾必要的结构推理和自动匹配的术语。我们的框架还可以处理类型理论的对应证明，有效地允许类型检查和建设的计算过程通过证明。我们演示了我们的实现使用一个简单的命题逻辑和Curry-Howard对应的Alzada演算，并认为它的使用与线性逻辑和它的各种对应的会话类型。
2021-01-11 cs.LO cs.SC
PSPACE Reasoning for Graded Modal Logics
本文给出了一个判定阶化模态逻辑Gr（K_R）可满足性的PSPACE算法，它是命题模态逻辑K_R通过计数表达式的自然推广，在知识表示领域中起着重要作用。该算法采用了tableaux的方法，是第一个已知的算法，满足问题的复杂性下限。因此，我们准确地解决了问题的复杂性，并驳斥了ExpTime-hardness猜想。我们将结果推广到逻辑Gr（K_（R \cap I））上，用逆关系和可达关系的交扩充了Gr（K_R）.这建立了一种“理论基准”，所有算法方法都可以根据它来衡量。
2000-05-08 cs.AI cs.CC cs.DS
