Related papers: A repetition-free hypersequent calculus for first-…
Public announcement logic(PAL) is an extension of epistemic logic (EL) with some reduction axioms. In this paper, we propose a cut-free labelled sequent calculus for PAL, which is an extension of that for EL with sequent rules adapted from…
Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic. In this paper, we compare three sequent…
LP$^{\supset,\mathsf{F}}$ is a three-valued paraconsistent propositional logic which is essentially the same as J3. It has most properties that have been proposed as desirable properties of a reasonable paraconsistent propositional logic.…
Glivenko's theorem states that a formula is derivable in classical propositional logic $\mathrm{CL}$ iff under the double negation it is derivable in intuitionistic propositional logic $\mathrm{IL}$: $\mathrm{CL}\vdash\varphi$ iff…
The displacement calculus $\mathbf{D}$ is a conservative extension of the Lambek calculus $\mathbf{L1}$ (with empty antecedents allowed in sequents). $\mathbf{L1}$ can be said to be the logic of concatenation, while $\mathbf{D}$ can be said…
We consider a many-sorted variant of Japaridze's polymodal provability logic $\mathsf{GLP}$. In this variant, which is denoted $\mathsf{GLP}^\ast$, propositional variables are assigned sorts $\alpha \leq \omega$, where variables of finite…
Sandqvist gave a proof-theoretic semantics (P-tS) for classical logic (CL) that explicates the meaning of the connectives without assuming bivalance. Later, he gave a semantics for intuitionistic propositional logic (IPL). While soundness…
We present a modification of the superposition calculus that is meant to generate consequences of sets of first-order axioms. This approach is proven to be sound and deductive-complete in the presence of redundancy elimination rules,…
In many instances in first order logic or computable algebra, classical theorems show that many problems are undecidable for general structures, but become decidable if some rigidity is imposed on the structure. For example, the set of…
Our main result is a new proof of correctness of Euclid's algorithm. The proof is conducted in algorithmic theory of natural numbers Th3. A formula H is constructed that expresses the halting property of the algorithm. Next, the proof of H…
Semiring semantics evaluates logical statements by values in some commutative semiring K. Random semiring interpretations, induced by a probability distribution on K, generalise random structures, and we investigate here the question of how…
First-order logic is the basis for many knowledge representation formalisms and methods. Providing technological support for learning to write first-order formulas for natural language specifications requires methods to test formulas for…
Nakano's "later" modality, inspired by G\"{o}del-L\"{o}b provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of…
We consider G\"odel temporal logic ($\sf GTL$), a variant of linear temporal logic based on G\"odel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a…
We present Generative Logic (GL), a deterministic architecture that starts from user-supplied axiomatic definitions written in a minimalist Mathematical Programming Language (MPL) and systematically explores a configurable region of their…
This Paper investigate sequent calculi for certain weak subintuitionistic logics. We establish that weakening and contraction are height-preserving admissible for each of these calculi, and we provide a syntactic proof for the admissibility…
This paper describes a general framework for automatic termination analysis of logic programs, where we understand by ``termination'' the finitenes s of the LD-tree constructed for the program and a given query. A general property of…
The automated theorem prover Leo-III for classical higher-order logic with Henkin semantics and choice is presented. Leo-III is based on extensional higher-order paramodulation and accepts every common TPTP dialect (FOF, TFF, THF),…
In this paper we study some fragments without implications of the (Hilbert) full Lambek logic $\mathbf{HFL}$ and also some fragments without implications of some of the substructural extensions of that logic. To do this, we perform an…
First-order multiplicative intuitionistic linear logic (MILL1) can be seen as an extension of the Lambek calculus. In addition to the fragment of MILL1 which corresponds to the Lambek calculus (of Moot & Piazza 2001), I will show fragments…