Related papers: Cyclic and Inductive Calculi are equivalent
We present a sequent-style proof system for provability logic GL that admits so-called circular proofs. For these proofs, the graph underlying a proof is not a finite tree but is allowed to contain cycles. As an application, we establish…
We introduce a logic for reasoning about evidence, that essentially views evidence as a function from prior beliefs (before making an observation) to posterior beliefs (after making the observation). We provide a sound and complete…
Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic proof system for symbolic heaps with general form of…
Propositional logics in general, considered as a set of sentences, can be undecidable even if they have "nice" representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already…
The purpose of this paper is to give an easy to understand with step-by-step explanation to allow interested people to fully appreciate the power of natural deduction for first-order logic. Natural deduction as a proof system can be used to…
We introduce a logic for reasoning about evidence that essentially views evidence as a function from prior beliefs (before making an observation) to posterior beliefs (after making the observation). We provide a sound and complete…
An inductive logic can be formulated in which the elements are not propositions or probability distributions, but information systems. The logic is complete for information systems with binary hypotheses, i.e., it applies to all such…
Chase algorithms are indispensable in the domain of knowledge base querying, which enable the extraction of implicit knowledge from a given database via applications of rules from a given ontology. Such algorithms have proved beneficial in…
We study induction on the program structure as a proof method for bisimulation-based compiler correctness. We consider a first-order language with mutually recursive function definitions, system calls, and an environment semantics. The…
We present a simpler way than usual to deduce the completeness theorem for the second-oder classical logic from the first-order one. We also extend our method to the case of second-order intuitionistic logic.
An increasing number of scientific experiments support the view of perception as Bayesian inference, which is rooted in Helmholtz's view of perception as unconscious inference. Recent study of logic presents a view of logical reasoning as…
Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization CL18 of the basic propositional fragment of computability…
It is common practice to compare the computational power of different models of computation. For example, the recursive functions are strictly more powerful than the primitive recursive functions, because the latter are a proper subset of…
Cirquent calculus is a new proof-theoretic and semantic approach introduced for the needs of computability logic by G.Japaridze, who also showed that, through cirquent calculus, one can capture, refine and generalize independence-friendly…
Dynamic logic is a modal logic for reasoning about programs. A cyclic proof system is a proof system that allows proofs containing cycles and is an alternative to a proof system containing (co-)induction. This paper introduces a sequent…
In answer set programming, two groups of rules are considered strongly equivalent if they have the same meaning in any context. Strong equivalence of two programs can be sometimes established by deriving rules of each program from rules of…
We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike $\lambda$-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names…
This work is meant to demonstrate new class of prime numbers -- cyclic prime numbers, that can be derived from any prime number at certain numeric systems. Cyclic prime numbers are also related to the cyclic numbers and full reptend prime…
We give a new proof of Brooks' theorem that immediately implies a strengthening of Brooks' theorem, known as Catlin's theorem.
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html). The logical vocabulary of the system consists of…