Defining a Resource-Sensitive Approximation Theory for the λμ-Calculus
The article proposes a resource-sensitive version of the λμ-calculus and defines a Taylor expansion for it, which provides a sensible approximation theory for the language and enables the proof of advanced properties such as Stability and Perpendicular Lines Property.
Stability Property for the Call-by-Value λ-Calculus Proven via Taylor Expansion
The Stability Property, which states necessary conditions under which the contexts of the Call-by-Value λ-calculus commute with intersections of approximants, is proven via the tool of resource approximation.
Exploring Denotational Semantics and Simplicial Homology for Analyzing Logical Proofs
The article proposes to study the external structure of logical proofs by interpreting them as faces of an abstract simplicial complex, and explores the use of simplicial homology to analyze the geometric properties of this representation.
Decidability of Querying First-Order Theories via Countermodels of Finite Width
The decidability of logical entailment problems can be established by exploiting the existence of countermodels that are structurally simple, as measured by certain types of width measures.
Efficient Counting of Minimal Models of Boolean Formulas via Knowledge Compilation
This work proposes a novel knowledge compilation approach, named KC-min, that enables efficient counting of minimal models of Boolean formulas.
Efficient Enumeration of Minimal Unsatisfiable Cores for Linear Temporal Logic over Finite Traces (LTLf) Formulas
This paper introduces a novel technique for efficiently enumerating minimal unsatisfiable cores (MUCs) of an LTLf specification by encoding it into an Answer Set Programming (ASP) specification, such that the minimal unsatisfiable subsets (MUSes) of the ASP program directly correspond to the MUCs of the original LTLf specification.
비-엄격 지시자를 포함한 모달 및 시간적 자유 기술 논리의 확장 버전
이 논문은 정의 기술과 개별 이름을 포함하는 모달 기술 논리를 제안하고, 이러한 논리의 결정가능성과 복잡도를 조사한다. 저자들은 일차 모달 논리의 한 변수 단편과 계수를 모달 기술 논리에 연결하고, 일부 기본적인 모달 논리에 대해 NEXPTIME 완전성 결과를 증명한다. 또한 일부 표현력 있는 논리가 상수 영역에서는 결정불가능하지만 확장 영역에서는 결정가능해진다는 것을 보여준다.
새로운 클론 이론을 위한 토폴로지 탐구
이 논문은 ω-연산과 ω-관계의 토폴로지와 대수적 연구를 제시한다. 특정 이상 X에 따라 ω-연산 집합에 X-토폴로지를 정의하고, X-다형성과 X-불변 관계를 소개한다. 또한 X-닫힌 ω-클론을 Polω-Invω로 특성화하고, Invω-Polω와 고전적인 Inv-Pol 사이의 관계를 제시한다.
Topological and Algebraic Study of Polymorphisms and Invariant Relations of Infinite Arity
This paper presents a topological and algebraic framework for studying polymorphisms and invariant relations of infinite arity (ω-operations and ω-relations). It introduces parametric topologies on the set of ω-operations and uses them to define ω-polymorphisms and ω-invariant relations. The authors characterize the closed ω-clones in terms of ω-polymorphisms and ω-invariant relations, and relate the Inv-Pol Galois connection for finite arity to the Invω-Polω connection for infinite arity.
A Three-Valued Parsing Algorithm for Boolean Grammars with Strong Negation
The authors present a GLR-like parsing algorithm for three-valued interpretations of Boolean grammars that can handle contradictory grammars using a three-valued logic approach.
© 2024 by Linnk AI