Ugo Dal Lago, Martin Hofmann
We present QBAL, an extension of Girard, Scedrov and Scott's bounded linear logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded linear logic considerably more flexible, while preserving soundness and completeness for polynomial time. In particular, we provide compositional embeddings of Leivant's RRW and Hofmann's LFPL into QBAL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Unification in Matching Logic -- Revisited
本文针对匹配逻辑中多结构模式需多次匹配的问题，在应用型匹配逻辑变体中推广合一问题，并在Coq中实现了经可靠性证明的合一机械化解决方案。
We present a unified approach to (both finite and unrestricted) worst-case optimal entailment of (unions of) conjunctive queries (U)CQs in the wide class of "locally-forward" description logics. The main technique that we employ is a generalisation of Lutz's spoiler technique, originally developed for CQ entailment in ALCHQ. Our result closes numerous gaps present in the literature, most notably implying ExpTime-completeness of (U)CQ-querying for any superlogic of ALC contained in ALCHbregQ, and, as we believe, is abstract enough to be employed as a black-box in many new scenarios.
The Modal Cube Revisited: Semantics without Worlds (Technical Report)
本文为模态立方体提出基于八值Nmatrices的非确定性语义框架，利用层级赋值捕获必然化，提供可靠完备判定程序，并解决非确定性下公理与语义条件对应关系的长期猜想。
Physically Aware Synthesis Revisited: Guiding Technology Mapping with Primitive Logic Gate Placement
针对VLSI设计前后端迭代成本高的问题，提出PigMAP框架，通过线长驱动的工艺映射生成物理友好网表，含性能和功耗两种模式，在EPFL基准上实现延迟与功耗的优化。
Conditional logics play an important role in recent attempts to formulate theories of default reasoning. This paper investigates first-order conditional logic. We show that, as for first-order probabilistic logic, it is important not to confound statistical conditionals over the domain (such as ``most birds fly''), and subjective conditionals over possible worlds (such as ``I believe that Tweety is unlikely to fly''). We then address the issue of ascribing semantics to first-order conditional logic. As in the propositional case, there are many possible semantics. To study the problem in a cohe…
Bounded model checking of pointer programs is a debugging technique for programs that manipulate dynamically allocated pointer structures on the heap. It is based on the following four observations. First, error conditions like dereference of a dangling pointer, are expressible in a~fragment of first-order logic with two-variables. Second, the fragment is closed under weakest preconditions wrt. finite paths. Third, data structures like trees, lists etc. are expressible by inductive predicates defined in a fragment of Datalog. Finally, the combination of the two fragments of the two-variable lo…
Theory of stable models is the mathematical basis of answer set programming. Several results in that theory refer to the concept of the positive dependency graph of a logic program. We describe a modification of that concept and show that the new understanding of positive dependency makes it possible to strengthen some of these results. Under consideration in Theory and Practice of Logic Programming (TPLP).
In earlier work, we proposed a logic that extends the Logic of General Awareness of Fagin and Halpern [1988] by allowing quantification over primitive propositions. This makes it possible to express the fact that an agent knows that there are some facts of which he is unaware. In that logic, it is not possible to model an agent who is uncertain about whether he is aware of all formulas. To overcome this problem, we keep the syntax of the earlier paper, but allow models where, with each world, a possibly different language is associated. We provide a sound and complete axiomatization for this l…
We analyze a model of interactive unawareness introduced by Heifetz, Meier and Schipper (HMS). We consider two axiomatizations for their model, which capture different notions of validity. These axiomatizations allow us to compare the HMS approach to both the standard (S5) epistemic logic and two other approaches to unawareness: that of Fagin and Halpern and that of Modica and Rustichini. We show that the differences between the HMS approach and the others are mainly due to the notion of validity used and the fact that the HMS is based on a 3-valued propositional logic.
The first-order theory of a string automatic structure is known to be decidable, but there are examples of string automatic structures with nonelementary first-order theories. We prove that the first-order theory of a string automatic structure of bounded degree is decidable in doubly exponential space (for injective automatic presentations, this holds even uniformly). This result is shown to be optimal since we also present a string automatic structure of bounded degree whose first-order theory is hard for 2EXPSPACE. We prove similar results also for tree automatic structures. These findings …
In this paper, we consider a method of computing minimal models in circumscription using integer programming in propositional logic and first-order logic with domain closure axioms and unique name axioms. This kind of treatment is very important since this enable to apply various technique developed in operations research to nonmonotonic reasoning. Nerode et al. (1995) are the first to propose a method of computing circumscription using integer programming. They claimed their method was correct for circumscription with fixed predicate, but we show that their method does not correctly reflect t…
Successor-Invariant First-Order Logic on Classes of Bounded Degree
本文研究后继不变一阶逻辑的表达能力，证明在有界度类上其表达能力不高于普通一阶逻辑。
Previous work has shown that reasoning with real-time temporal logics is often simpler when restricted to models with bounded variability---where no more than v events may occur every V time units, for given v, V. When reasoning about formulas with intrinsic bounded variability, one can employ the simpler techniques that rely on bounded variability, without any loss of generality. What is then the complexity of algorithmically deciding which formulas have intrinsic bounded variability? In this paper, we study the problem with reference to Metric Temporal Logic (MTL). We prove that deciding bou…
We present CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. Even for decidable constraint systems, satisfiability and Model Checking problem of such logic can be undecidable. We introduce suitable restrictions and assumptions that are shown to make the satisfiability problem for the extended logic decidable. Moreover for a large class of constraint systems we propose an encoding that realize an effective decision procedure for the Bounded Reachability problem.
Recursive windows for grammar logics of bounded density
本文推广有限窗口提出递归窗口方法，研究有界密度多模态逻辑，证明其可满足性问题是 PSPACE-完全的，并证明密度单模态逻辑属于 para-PSPACE。
Temporal Team Semantics Revisited
本文提出基于时间评估函数的时间团队语义学，用于规范异步超属性，并证明同步TeamLTL的嵌入、某些TeamCTL片段MC的高度不可判定性，以及TeamCTL*到交替异步Büchi自动机的翻译及可判定性结果。
Bounded Inquisitive Logics: Sequent Calculi and Schematic Validity
本文为 n-有界探究逻辑 InqBQ_n 构造了无切割带标签矢列演算，并通过 Casari 公式揭示了原子有效性与模式有效性在有界与无界谓词探究逻辑中的微妙差异。
Order-invariant cluster first-order logic on graph classes of bounded degree
本文提出一种新的逻辑，用于研究图类有界度上的顺序不变性，展示其在该类图中表达能力不超越一阶逻辑。
First Order Logic on Pathwidth Revisited Again
研究有界路径宽度图上一阶逻辑可表达性质的可判定性，证明其具有初等依赖，与树宽度情况形成对比。
Parameterized algorithms are a way to solve hard problems more efficiently, given that a specific parameter of the input is small. In this paper, we apply this idea to the field of answer set programming (ASP). To this end, we propose two kinds of graph representations of programs to exploit their treewidth as a parameter. Treewidth roughly measures to which extent the internal structure of a program resembles a tree. Our main contribution is the design of parameterized dynamic programming algorithms, which run in linear time if the treewidth and weights of the given program are bounded. Compa…
Dynamic Epistemic Logic of Resource Bounded Information Mining Agents
本文提出资源受限智能体半公开查询的动态认知逻辑，刻画付费私密答案、预算约束与群体共享资源查询，并证明其完备性、可判定性及高效模型检测。
This paper extends prior work on the connections between logics from finite model theory and propositional/algebraic proof systems. We show that if all non-isomorphic graphs in a given graph class can be distinguished in the logic Choiceless Polynomial Time with counting (CPT), then they can also be distinguished in the bounded-degree extended polynomial calculus (EPC), and the refutations have roughly the same size as the resource consumption of the CPT-sentence. This allows to transfer lower bounds for EPC to CPT and thus constitutes a new potential approach towards better understanding the …
Preservation theorems on sparse classes revisited
该研究重新审视稀疏结构类上一阶逻辑的同态保持定理，指出原有证明中可加性假设强度不足，构造了有界树宽的反例并证明平面图类不满足该性质，同时提出用瓶颈合并条件替代可加性以恢复证明有效性。
We study the expressive power and succinctness of order-invariant sentences of first-order (FO) and monadic second-order (MSO) logic on structures of bounded tree-depth. Order- invariance is undecidable in general and, thus, one strives for logics with a decidable syntax that have the same expressive power as order-invariant sentences. We show that on structures of bounded tree-depth, order-invariant FO has the same expressive power as FO. Our proof technique allows for a fine-grained analysis of the succinctness of this translation. We show that for every order-invariant FO sentence there exi…
Bounded Modal Logic: Explicit Scope Dependencies in Multi-Stage Programming
有界模态逻辑通过结合直觉和模态转换，提供细粒度资源控制的理论支持。
In recent work, comonads and associated structures have been used to analyse a range of important notions in finite model theory, descriptive complexity and combinatorics. We extend this analysis to Hybrid logic, a widely-studied extension of basic modal logic, which corresponds to the bounded fragment of first-order logic. In addition to characterising the various resource-indexed equivalences induced by Hybrid logic and the bounded fragment, and the associated combinatorial decompositions of structures, we also give model-theoretic characterisations of bounded formulas in terms of invariance…
A Finite-Model-Theoretic View on Propositional Proof Complexity
本文建立了命题证明系统（如Horn归结、有界宽度归结、有界次多项式演算）与有限模型论中不动点逻辑之间的紧密对应关系，并利用这些联系为多项式演算证明下界提供了新工具。
Timed Automata (TA) are a very popular modeling formalism for systems with time-sensitive properties. A common task is to verify if a network of TA satisfies a given property, usually expressed in Linear Temporal Logic (LTL), or in a subset of Timed Computation Tree Logic (TCTL). In this paper, we build upon the TACK bounded model checker for TA, which supports a signal-based semantics of TA and the richer Metric Interval Temporal Logic (MITL). TACK encodes both the TA network and property into a variant of LTL, Constraint LTL over clocks (CLTLoc). The produced CLTLoc formula can then be solve…
Local-Order-Invariant Logic on Classes of Bounded Degree
本文研究了有限度类上的局部顺序不变逻辑，证明其退化为一阶逻辑，并探讨了epsilon不变逻辑的上界。
A Bitopological Approach to Finite Reduction and Bounded Exact-Value Certificates for Fitting's Finite Heyting-valued Modal Logic
针对菲廷有限海廷值模态逻辑，采用关系双拓扑表示法获得有限状态归约，构造受模态深度约束的有限树状精确值证书，实现保留精确真值的极小满射归约与有界归约反例。
The parameterized space complexity of model-checking bounded variable first-order logic
本文研究有界变量一阶查询模型检测的参数化空间复杂度，建立树层次结构完备性，提出高空间效率检测器，并探讨其最优性。
We prove that, on bounded expansion classes, every first-order formula with modulo counting is equivalent, in a linear-time computable monadic expansion, to an existential first-order formula. As a consequence, we derive, on bounded expansion classes, that first-order transductions with modulo counting have the same encoding power as existential first-order transductions. Also, modulo-counting first-order model checking and computation of the size of sets definable in modulo-counting first-order logic can be achieved in linear time on bounded expansion classes. As an application, we prove that…
One of the central open questions in bounded arithmetic is whether Buss' hierarchy of theories of bounded arithmetic collapses or not. In this paper, we reformulate Buss' theories using free logic and conjecture that such theories are easier to handle. To show this, we first prove that Buss' theories prove consistencies of induction-free fragments of our theories whose formulae have bounded complexity. Next, we prove that although our theories are based on an apparently weaker logic, we can interpret theories in Buss' hierarchy by our theories using a simple translation. Finally, we investigat…
Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic (RB-ATL) is decidable. However, for coalition logics with unbounded resource production and consumption, only some undecidability results are known…
We investigate the proof complexity of extended Frege (EF) systems for basic transitive modal logics (K4, S4, GL, ...) augmented with the bounded branching axioms $\mathbf{BB}_k$. First, we study feasibility of the disjunction property and more general extension rules in EF systems for these logics: we show that the corresponding decision problems reduce to total coNP search problems (or equivalently, disjoint NP pairs, in the binary case); more precisely, the decision problem for extension rules is equivalent to a certain special case of interpolation for the classical EF system. Next, we use…
Depth-bounded epistemic logic
本文提出深度有界认知逻辑DBEL及其公开宣告扩展DPAL，模拟智能体仅能推理有限模态深度的公式，给出公理化与复杂性结果，并应用于泥孩子问题以刻画所需深度知识界限。
Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations
本文研究关系分离逻辑SLR的MSO可定义性，提出一个可描述有界树宽图集合并能有效翻译为MSO的表达性片段，从而保证可满足性与蕴含问题的可判定性。
pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
提出pacSTL框架，结合PAC有界可达集预测与区间STL，通过优化问题计算原子鲁棒性上下界并传播，实现规范级别的PAC有界鲁棒性评估，用于不确定动态系统的验证与监控。
We study two unary fragments of the well-known metric interval temporal logic MITL[U_I,S_I] that was originally proposed by Alur and Henzinger, and we pin down their expressiveness as well as satisfaction complexities. We show that MITL[F_\inf,P_\inf] which has unary modalities with only lower-bound constraints is (surprisingly) expressively complete for Partially Ordered 2-Way Deterministic Timed Automata (po2DTA) and the reduction from logic to automaton gives us its NP-complete satisfiability. We also show that the fragment MITL[F_b,P_b] having unary modalities with only bounded intervals h…
We describe ongoing work on a framework for automatic composition synthesis from a repository of software components. This work is based on combinatory logic with intersection types. The idea is that components are modeled as typed combinators, and an algorithm for inhabitation {\textemdash} is there a combinatory term e with type tau relative to an environment Gamma? {\textemdash} can be used to synthesize compositions. Here, Gamma represents the repository in the form of typed combinators, tau specifies the synthesis goal, and e is the synthesized program. We illustrate our approach by examp…
We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $Σ_1$ theory is undecidable (already over two letters). We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the $Σ_1$ fragment is decidable, and that it becomes undecidable when three variab…
Alloy is formal modeling language based on first-order relational logic, with no specific support for specifying reactive systems. We propose the usage of temporal logic to specify such systems, and show how bounded model checking can be performed with the Alloy Analyzer.
In this paper, we study Reiter's propositional default logic when the treewidth of a certain graph representation (semi-primal graph) of the input theory is bounded. We establish a dynamic programming algorithm on tree decompositions that decides whether a theory has a consistent stable extension (Ext). Our algorithm can even be used to enumerate all generating defaults (ExtEnum) that lead to stable extensions. We show that our algorithm decides Ext in linear time in the input theory and triple exponential time in the treewidth (so-called fixed-parameter linear algorithm). Further, our algorit…
We provide a logical framework in which a resource-bounded agent can be seen to perform approximations of probabilistic reasoning. Our main results read as follows. First we identify the conditions under which propositional probability functions can be approximated by a hierarchy of depth-bounded Belief functions. Second we show that under rather palatable restrictions, our approximations of probability lead to uncertain reasoning which, under the usual assumptions in the field, qualifies as tractable.
Depth-bounded Epistemic Logic
本文提出限制智能体模态推理深度的 DBEL 与支持公开宣告的 DPAL，给出公理化和复杂性结果，并以泥孩问题刻画所需深度知识的界。
Frick and Grohe [J. ACM 48 (2006), 1184-1206] introduced a notion of graph classes with locally bounded tree-width and established that every first order logic property can be decided in almost linear time in such a graph class. Here, we introduce an analogous notion for matroids (locally bounded branch-width) and show the existence of a fixed parameter algorithm for first order logic properties in classes of regular matroids with locally bounded branch-width. To obtain this result, we show that the problem of deciding the existence of a circuit of length at most k containing two given element…
Computational trust mechanisms aim to produce trust ratings from both direct and indirect information about agents' behaviour. Subjective Logic (SL) has been widely adopted as the core of such systems via its fusion and discount operators. In recent research we revisited the semantics of these operators to explore an alternative, geometric interpretation. In this paper we present a principled desiderata for discounting and fusion operators in SL. Building upon this we present operators that satisfy these desirable properties, including a family of discount operators. We then show, through a ri…
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。