相关论文: A System of Interaction and Structure

A logic is presented for reasoning on iterated sequences of formulae over some given base language. The considered sequences, or "schemata", are defined inductively, on some algebraic structure (for instance the natural numbers, the lists,…

Motivated by some recent developments in abstract theories of quadratic forms, we start to develop in this work an expansion of Linear Algebra to multivalued structures (a multialgebraic structure is essentially an algebraic structure but…

A many-valued modal logic is introduced that combines the usual Kripke frame semantics of the modal logic K with connectives interpreted locally at worlds by lattice and group operations over the real numbers. A labelled tableau system is…

In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton's Linear/Non-Linear Logic by removing the existence of the exchange structural rule. One should…

Separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called…

Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The graded "of-course" modality $!_r$ captures how many times a…

We introduce a family of comparative plausibility logics over neighbourhood models, generalising Lewis' comparative plausibility operator over sphere models. We provide axiom systems for the logics, and prove their soundness and…

It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof of a proposition P by the proof of an…

We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong L\"ob logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A…

The foundational character of certain algebraic structures as Boolean algebras and Heyting algebras is rooted in their potential to model classical and constructive logic, respectively. In this paper we discuss the contributions of…

We introduce Bifurcation Logic, BL, which combines a basic classical modality with separating conjunction * together with its naturally associated multiplicative implication, that is defined using the modal ordering. Specifically, a formula…

It is shown the construction of a module structure [2] with universe over a set of a particular kind of mathematical proofs, the base ring of this module will be built on a maximal consistent extension of a set of propositions, this…

We establish a novel connection between two research areas in non-classical logics which have been developed independently of each other so far: on the one hand, input/output logic, introduced within a research program developing logical…

Linear logic has provided new perspectives on proof-theory, denotational semantics and the study of programming languages. One of its main successes are proof-nets, canonical representations of proofs that lie at the intersection between…

There is a generic way to add any new feature to a system. It involves 1) identifying the basic units which build up the system and 2) introducing the new feature to each of these basic units. In the case where the system is argumentation…

Cut-elimination is the bedrock of proof theory. It is the algorithm that eliminates cuts from a sequent calculus proof that leads to cut-free calculi and applications. Cut-elimination applies to many logics irrespective of their semantics.…

Input/Output (I/O) logic is a general framework for reasoning about conditional norms and/or causal relations. We streamline Bochman's causal I/O logics via proof-search-oriented sequent calculi. Our calculi establish a natural syntactic…

Modular structure is pervasive in many complex networks of interactions observed in natural, social and technological sciences. Its study sheds light on the relation between the structure and function of complex systems. Generally speaking,…

We present a unified theory for formal mathematical systems including recursive systems closely related to formal grammars, including the predicate calculus as well as a formal induction principle. We introduce recursive systems generating…

Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal…