Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDiagrammatic Inference
125
0
0.0
(
0
)
Added by
Dominique Duval
Publication date
2009
fields
Informatics Engineering
and research's language is
English
Authors
Dominique Duval
Ask ChatGPT about the research
No Arabic abstract
Diagrammatic logics were introduced in 2002, with emphasis on the notions of specifications and models. In this paper we improve the description of the inference process, which is seen as a Yoneda functor on a bicategory of fractions. A diagrammatic logic is defined from a morphism of limit sketches (called a propagator) which gives rise to an adjunction, which in turn determines a bicategory of fractions. The propagator, the adjunction and the bicategory provide respectively the syntax, the models and the inference process for the logic. Then diagrammatic logics and their morphisms are applied to the semantics of side effects in computer languages.
rate research
Read More
This paper is a submission to the contest: How to combine logics? at the World Congress and School on Universal Logic III, 2010. We claim that combining things, whatever these things are, is made easier if these things can be seen as the objects of a category. We define the category of diagrammatic logics, so that categorical constructions can be used for combining diagrammatic logics. As an example, a combination of logics using an opfibration is presented, in order to study computational side-effects due to the evolution of the state during the execution of an imperative program.
Although automated reasoning with diagrams has been possible for some years, tools for diagrammatic reasoning are generally much less sophisticated than their sentential cousins. The tasks of exploring levels of automation and abstraction in the construction of proofs and of providing explanations of solutions expressed in the proofs remain to be addressed. In this paper we take an interactive proof assistant for Euler diagrams, Speedith, and add tactics to its reasoning engine, providing a level of automation in the construction of proofs. By adding tactics to Speediths repertoire of inferences, we ease the interaction between the user and the system and capture a higher level explanation of the essence of the proof. We analysed the design options for tactics by using metrics which relate to human readability, such as the number of inferences and the amount of clutter present in diagrams. Thus, in contrast to the normal case with sentential tactics, our tactics are designed to not only prove the theorem, but also to support explanation.
In this paper we consider the two major computational effects of states and exceptions, from the point of view of diagrammatic logics. We get a surprising result: there exists a symmetry between these two effects, based on the well-known categorical duality between products and coproducts. More precisely, the lookup and update operations for states are respectively dual to the throw and catch operations for exceptions. This symmetry is deeply hidden in the programming languages; in order to unveil it, we start from the monoidal equational logic and we add progressively the logical features which are necessary for dealing with either effect. This approach gives rise to a new point of view on states and exceptions, which bypasses the problems due to the non-algebraicity of handling exceptions.
The word problem for categories with free products and coproducts (sums), SP-categories, is directly related to the problem of determining the equivalence of certain processes. Indeed, the maps in these categories may be directly interpreted as processes which communicate by two-way channels. The maps of an SP-category may also be viewed as a proof theory for a simple logic with a game theoretic intepretation. The cut-elimination procedure for this logic determines equality only up to certain permuting
Deduction systems and graph rewriting systems are compared within a common categorical framework. This leads to an improved deduction method in diagrammatic logics.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
