相关论文: A diagrammatic calculus of n-term syllogisms

A diagrammatic logical calculus for the syllogistic reasoning is introduced and discussed. We prove that a syllogism is valid if and only if it is provable in the calculus.

In this paper, we deal with a calculus system SLCD (Syllogistic Logic with Carroll Diagrams), which gives a formal approach to logical reasoning with diagrams, for representations of the fundamental Aristotelian categorical propositions and…

Diagram chasing is not an easy task. The coherence holds in a generalized sense if we have a mechanical method to judge whether given two morphisms are equal to each other. A simple way to this end is to reform a concerned category into a…

We present a reading of the traditional syllogistics in a fragment of the propositional intuitionistic multiplicative linear logic and prove that with respect to a diagrammatic logical calculus that we introduced in a previous paper, a…

This paper explores relational syllogistic logics, a family of logical systems related to reasoning about relations in extensions of the classical syllogistic. These are all decidable logical systems. We prove completeness theorems and…

Inclusion diagrams are introduced as an alternative to using Venn diagrams to determine the validity of categorical syllogisms, and are used here for the analysis of diverse categorical syllogisms. As a preliminary example of a possible…

We consider sentence-definable and diagram-definable subfamilies of given families of theories, calculi for these subfamilies, as well dynamics and characteristics of these subfamilies with respect to rank and degree.

We introduce a class of rooted graphs which allows one to encode various kinds of classical or quantum circuits. We then follow a set-theoretic approach to define rewrite systems over the considered graphs and propose a new complete…

Deduction systems and graph rewriting systems are compared within a common categorical framework. This leads to an improved deduction method in diagrammatic logics.

We develop a rewriting theory suitable for diagrammatic algebras and lay down the foundations of a systematic study of their higher structures. In this paper, we focus on the question of finding bases. As an application, we give the first…

This paper presents general syntactic conditions ensuring the strong normalization and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined…

We verify a confluence result for the rewriting calculus of the linear category introduced in our previous paper. Together with the termination result proved therein, the generalized coherence theorem for linear category is established.…

We introduce the calculus of neo-Peircean relations, a string diagrammatic extension of the calculus of binary relations that has the same expressivity as first order logic and comes with a complete axiomatisation. The axioms are obtained…

This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more…

We introduce ologisms. They generate from ologs by extending their logical expressivity, from the possibility of considering constraints of equational nature only to the possibility of considering constraints of syllogistic nature, in…

Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity…

We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these…

We propose a modal logic tailored to describe graph transformations and discuss some of its properties. We focus on a particular class of graphs called termgraphs. They are first-order terms augmented with sharing and cycles. Termgraphs…

A coherent presentation of an n-category is a presentation by generators, relations and relations among relations. Confluent and terminating rewriting systems generate coherent presentations, whose relations among relations are defined by…

In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce a set of logical connectives allowing us to extend the correspondence between cographs and classical propositional formulas to any…