Multi-adjoint logic programming is a general framework with interesting features, which involves other positive logic programming frameworks such as monotonic and residuated logic programming, generalized annotated logic programs, fuzzy logic programming and possibilistic logic programming. One of the most interesting extensions of this framework is the possibility of considering a negation operator in the logic programs, which will improve its flexibility and the range of real applications.
This paper introduces multi-adjoint normal logic programming, which is an extension of multi-adjoint logic programming including a negation operator in the underlying lattice. Beside the introduction of the syntax and semantics of this paradigm, we will provide sufficient conditions for the existence of stable models defined on a convex compact set of a euclidean space. Finally, we will consider a particular algebraic structure in which sufficient conditions can be given in order to ensure the unicity of stable models of multi-adjoint normal logic programs.
Technically speaking, the transcendental syntax is about designing logics with a computational foundation. It suggests a new framework for proof theory where logic (proofs, formulas, truth, ...) is no more primitive but computation is. All the logical entities and activities will be presented as formatting/structuring on a given model of computation which should be as general, simple and natural as possible. The selected ground for logic in the transcendental syntax is a model of computation I call "stellar resolution" which is basically a logic-free reformulation of Robinson's first-order cla…
We develop a classical propositional logic for reasoning about combinatory logic. We define its syntax, axiomatic system and semantics. The syntax and axiomatic system are presented based on classical propositional logic, with typed combinatory terms as basic propositions, along with the semantics based on applicative structures extended with special elements corresponding to primitive combinators. Both the equational theory of untyped combinatory logic and the proposed axiomatic system are proved to be sound and complete w.r.t. the given semantics. In addition, we prove that combinatory logic…
We introduce a new logic that combines Adjoint Logic with Graded Necessity Modalities. This results in a very expressive system capable of controlling when and how structural rules are used. We give a sequent calculus, natural deduction, and term assignment for Graded Adjoint Logic.
Variable types for meaning assembly: a logical syntax for generic noun phrases introduced by most
Université de Bordeaux（波尔多大学）；CNRS（法国国家科学研究中心）
本文提出了一种计算类属名词短语与广义量词最对应的句子的语义的方法。我们称这些泛型为样本，它们类似于词汇语义学中的原型或原型。这些意义被视为逻辑公式，此后可以在您最喜欢的模型中进行解释。为了做到这一点，我们与主流的弗雷根观点有很大的不同，弗雷根认为宇宙是一个单一的无类型宇宙。事实上，我们的建议采用了类型论，并从希尔伯特ε-微积分（Hilbert，1922; Avigad and Zach，2008）和中世纪哲学中得到了一些提示，例如de Libera（1993，1996）。我们的类型理论分析与正在进行的词汇语义学研究有一些相似之处（Asher 2011; Bassac et al. 2010; Moot，Précourt and Retoré 2011）。我们的模型也适用于经典的例子，涉及一个类，或这个类的通用元素，这是不是说出，但提供的上下文。本研究的一个结果是，在最低限度主义-语境主义的争论中，参见Conrad（2011），如果采用类型理论的观点，术语编码纯粹的语义成分，而它们的类型是由语用决定的。
The set of integer number lists with finite length, and the set of binary trees with integer labels are both countably infinite. Many inductively defined types also have countably many elements. In this paper, we formalize the syntax of first order inductive definitions in Coq and prove them countable, under some side conditions. Instead of writing a proof generator in a meta language, we develop an axiom-free proof in the Coq object logic. In other words, our proof is a dependently typed Coq function from the syntax of the inductive definition to the countability of the type. Based on this pr…
Center for Information and Bubble Studies, University of Copenhagen（哥本哈根大学信息与泡沫研究中心）
The literature on awareness modeling includes both syntax-free and syntax-based frameworks. Heifetz, Meier \& Schipper (HMS) propose a lattice model of awareness that is syntax-free. While their lattice approach is elegant and intuitive, it precludes the simple option of relying on formal language to induce lattices, and does not explicitly distinguish uncertainty from unawareness. Contra this, the most prominent syntax-based solution, the Fagin-Halpern (FH) model, accounts for this distinction and offers a simple representation of awareness, but lacks the intuitiveness of the lattice structur…
Handsome proof nets were introduced by Retoré as a syntax for multiplicative linear logic. These proof nets are defined by means of cographs (graphs representing formulas) equipped with a vertices partition satisfying simple topological conditions. In this paper we extend this syntax to multiplicative linear logic with units and exponentials. For this purpose we develop a new sound and complete sequent system for the logic, enforcing a stronger notion of proof equivalence with respect to the one usually considered in the literature. We then define combinatorial proofs, a graphical proof system…
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and domain-specific deductive and calculational support. The new store model yields clean separations and dynamic local views of variables, e.g. discrete/continuous, mutable/immutable, program/logical, and enhanced ways of manipulating them using combinators, projections and framing. This leads to more local inference rules, procedures and tactics for reasoning w…
Logic has proved essential for formally modeling software based systems. Such formal descriptions, frequently called specifications, have served not only as requirements documentation and formalisation, but also for providing the mathematical foundations for their analysis and the development of automated reasoning tools. Logic is usually studied in terms of its two inherent aspects: syntax and semantics. The relevance of the latter resides in the fact that producing logical descriptions of real-world phenomena, requires people to agree on how such descriptions are to be interpreted and unders…
Hybrid probabilistic logic programs can represent several scenarios thanks to the expressivity of Logic Programming extended with facts representing discrete and continuous distributions. The semantics for this type of programs is crucial since it ensures that a probability can be assigned to every query. Here, following one recent semantics proposal, we illustrate a concrete syntax, and we analyse the syntactic requirements needed to preserve the well-definedness.
We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a functor F into the syntax is stable over the codomain of F. We rely on the internal language of presheaf categories. In order to combine the internal languages of multiple presheaf categories, we use Dependent Right Adjoints and Multimodal Type Theory. Categorical gluing is used to prove these induction principles, but it not visible in their statements, which involve a notion of model without context extensions. As exam…
The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks
各种逻辑框架支持使用高阶抽象语法（HOAS）来表示形式化系统。虽然这些系统表面上看起来是相同的，但它们在许多方面不同;例如，它们如何处理假设的上下文，以及关于给定形式系统的哪些定理可以简洁地表达和证明。我们在本文中的贡献是三方面的：1）我们开发了一个共同的基础设施，用于表示基准的系统支持推理与绑定器，2）我们提出了几个具体的基准，突出了各种不同方面的推理的背景下的假设，和3）我们设计了一个开放的知识库ORBI，（开放的挑战问题库系统支持推理与绑定器）。我们的工作为不同系统的定性比较奠定了基础。这使我们能够回顾和调查最先进的技术，我们在本文的第2部分中对四个系统进行了详细的介绍（Festival et al，2015）。它还使我们能够概述未来的基础研究问题，关于元推理系统的设计和实现。
