Related papers: Proof-graphs for Minimal Implicational Logic
The syntactic nature of logic and computation separates them from other fields of mathematics. Nevertheless, syntax has been the only way to adequately capture the dynamics of proofs and programs such as cut-elimination, and the finiteness…
We introduce a new formalism for representing proofs in propositional logic called "scroll nets". Its fundamental construct is the "scroll", a topological notation for implication proposed by C. S. Peirce at the end of the 19th century as…
In this article we develop a new version of the intuitionist existential graphs presented by Arnol Oostra [4]. The deductive rules presented in this article have the same meaning as those described in the work of Yuri Poveda [5], because…
A previous article shows that any linear height bounded normal proof of a tautology in the Natural Deduction for Minimal implicational logic $M_{\supset}$ is as huge as it is redundant. More precisely, any proof in a family of…
The recommendation system is not only a problem of inductive statistics from data but also a cognitive task that requires reasoning ability. The most advanced graph neural networks have been widely used in recommendation systems because…
This work introduces a framework for quantifying the information content of logical propositions through the use of implication hypergraphs. We posit that a proposition's informativeness is primarily determined by its relationships with…
Traditional treatments of formal logic provide: 1. A syntax for formulas. 2. An inference relation between sets of formulas. 3. A rule for assigning meaning to formulas (semantics) that is sound with respect to the inference relation. First…
Based on an analysis of the inference rules used, we provide a characterization of the situations in which classical provability entails intuitionistic provability. We then examine the relationship of these derivability notions to uniform…
Uniform proofs are sequent calculus proofs with the following characteristic: the last step in the derivation of a complex formula at any stage in the proof is always the introduction of the top-level logical symbol of that formula. We…
Models of complex systems are widely used in the physical and social sciences, and the concept of layering, typically building upon graph-theoretic structure, is a common feature. We describe an intuitionistic substructural logic called…
Compact closed categories provide a foundational formalism for a variety of important domains, including quantum computation. These categories have a natural visualisation as a form of graphs. We present a formalism for equational reasoning…
This report defines (plain) Dag-like derivations in the purely implicational fragment of minimal logic $M_{\supset}$. Introduce the horizontal collapsing set of rules and the algorithm {\bf HC}. Explain why {\bf HC} can transform any…
We investigate some basic questions about the interaction of regular and rational relations on words. The primary motivation comes from the study of logics for querying graph topology, which have recently found numerous applications. Such…
Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this paper, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using…
Proofs are traditionally syntactic, inductively generated objects. This paper reformulates first-order logic (predicate calculus) with proofs which are graph-theoretic rather than syntactic. It defines a combinatorial proof of a formula…
Pull-tabbing is an evaluation approach for functional logic computations, based on a graph transformation recently proposed, which avoids making irrevocable non-deterministic choices that would jeopardize the completeness of computations.…
It has been argued that reduction procedures are closely connected to the question about identity of proofs and that accepting certain reductions would lead to a trivialization of identity of proofs in the sense that every derivation of the…
In this work we propose a multi-valued extension of logic programs under the stable models semantics where each true atom in a model is associated with a set of justifications. These justifications are expressed in terms of causal graphs…
Automated theorem proving in first-order logic is an active research area which is successfully supported by machine learning. While there have been various proposals for encoding logical formulas into numerical vectors -- from simple…
With help of a compact Prolog-based theorem prover for Intuitionistic Propositional Logic, we synthesize minimal assumptions under which a given formula formula becomes a theorem. After applying our synthesis algorithm to cover basic…