An abstracted version of this paper, entitled "Dialectical Program Semantics", was accepted for presentation at the 1st International Conference on Algebraic Methodology and Software Technology (AMAST'89), University of Iowa, Iowa City, Iowa, 1989
Dialectical logic is the logic of dialectical processes. The goal of dialectical logic is to introduce dynamic notions into logical computational systems. The fundamental notions of proposition and truth-value in standard logic are subsumed by the notions of process and flow in dialectical logic. Dialectical logic has a standard aspect, which can be defined in terms of the "local cartesian closure" of subtypes. The standard aspect of dialectical logic provides a natural program semantics which incorporates Hoare's precondition/postcondition semantics and extends the standard Kripke semantics of dynamic logic. The goal of the standard aspect of dialectical logic is to unify the logic of small-scale and large-scale programming.
An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic
University of Luxembourg, Department of Computer Science（卢森堡大学计算机科学系）；Universität Greifswald, Institut für Mathematik und Informatik（格赖夫斯瓦尔德大学数学与信息学研究所）
Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have been identified in the literature, among them the limited expressiveness, the lack of quantitative features, and the inability to express robustness. There is work on overcoming these shortcomings, but each of these is typically addressed in isolation. This is insufficient for applications where all shortcomings manifest themselves simultaneously. Here, we tackle this issue by introducing logics that address more than…
本文主要研究模态依赖逻辑.它是由Jouko Vääanänen在2007年引入的，作为一阶的扩展（分别为。模态）逻辑的依赖运算符=（）。一阶（resp.）命题）变量x_1，...，x_n，=（x_1，...，x_n）直观地说明x_n的值由x_1，.，x_n-1。我们认为片段的模态依赖逻辑通过限制允许模态和命题连接词的集合。我们对这些片段的可满足性和模型检查问题的复杂性进行了分类。对于可满足性，我们获得了从P over NP，Sigma_P^2和PSPACE到NEXP的复杂度，而对于模型检查，我们只根据它们的易处理性对片段进行分类，即我们在P中显示NP-完全性或包含性。对于这个扩展，我们再次分类的复杂性模型检查问题的片段。在这里，我们获得了从P over NP和coNP到PSPACE的复杂度。最后，我们分析了一阶依赖逻辑、独立友好逻辑及其二元片段。我们证明了两个变量的依赖逻辑的可满足性是NEXP-完全的，而两个变量的独立友好的逻辑，它是不可判定的，并使用这一点来证明，后者也比前者更有表现力。
This paper proposes first-order modal $ξ$-calculus as well as genealogical Kripke models. Inspired by modal $μ$-calculus, first-order modal $ξ$-calculus takes a quite similar form and extends its inductive expressivity onto a different dimension. We elaborate on several vivid examples that demonstrate this logic's profound utility, especially for depicting genealogy of concurrent computer processes. Bisimulation notion for the logic has also been thoroughly examined.
During the design of autonomous vehicles (AVs), several stages should include a verification process to guarantee that the AV is driving safely on the roads. One of these stages is to assure the AVs abide by the road traffic rules. To include road traffic rules in the design of an AV, a precise and unambiguous formalisation of these rules is needed. However, only recently this has been pointed out as an issue for the design of AVs and the few works on this only capture the temporal aspects of the rules, leaving behind the spatial aspects. Here, we extend the spatial traffic logic, Urban Multi-…
Dynamics and uncertainty are essential features of real-life argumentation, and many recent studies have focused on integrating both aspects into Dung's well-known abstract Argumentation Frameworks (AFs). This paper proposes a combination of the two lines of research through a well-behaved logical tool: Dynamic Logic of Propositional Assignments (DL-PA). Our results show that the main reasoning tasks of virtually all existing formalisms qualitatively representing uncertainty about AFs are encodable in DL-PA. Moreover, the same tool is also useful for capturing dynamic structures, such as contr…
Computational Aspects of the Calculus of Structure
Universidade Federal de Minas Gerais（米纳斯吉拉斯联邦大学）
逻辑是正确推理的科学，逻辑系统是用正确的方法证明一定逻辑中的断言的工具。有许多逻辑系统，以及许多形式化它们的方法，例如，使用自然演绎或微积分。结构演算（Calculus of Structures，CoS）是由Alessio Guglielmi在2004年提出的一种新的形式主义，它在推理规则可以应用于公式内部的任何深度的意义上推广了结构演算，而不仅仅是主要的连接词。有了这个特性，CoS中的证明比任何其他支持分析证明的形式主义都要短。虽然拥有CoS的自由和表现力是很好的，但从证明搜索的角度来看，更多的自由意味着更大的搜索空间。在寻找演绎系统的完全自动化时，这应该受到限制。人们做了一些努力来减少这种非确定性，但它们基本上都是可操作的方法，到目前为止，还没有关于CoS计算行为的坚实的理论结果。本论文的主要焦点是讨论如何提出一个适合于实现的CoS证明搜索策略。这一战略应该是理论性的，而不是纯粹的操作性的。我们引入了结构内部子结构的不相干数的概念，并使用这个概念来实现我们的主要结果：根据我们的猜想，有一个算法对应于一个证明搜索策略，每个可证明结构的子系统中的FBV（乘法线性逻辑MLL加上规则混合）只包含成对不同的原子。我们的算法实现，我们相信我们的策略是一个很好的起点，利用计算方面的CoS在更一般的系统，如BV本身。
(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems. In this paper we introduce an abstract theoretical framework for the systematic investigation of the logical aspects of closure spaces. To this end, we introduce the notion of closure (hyper)doctrines, i.e. doctrines endowed with inflationary operators (and subject to suitable conditions). The generality and effectiveness of this concept is witnessed by many examples arising naturally from …
