Inductive definitions are ubiquitous in mathematics and computer science, and play an important role in knowledge representation. To date, several proof systems have been developed for inductive definitions. However, these systems are typically ...

Recently, the authors identified the “logical essence” of the call-by-value CPS translation to be its decomposition into two translations: a map into a fragment of the sequent calculus LJQ already determining the same semantics as CPS; and a later, ...

Choice logics constitute a family of propositional logics and are used for the representation of preferences, with especially qualitative choice logic (QCL) being an established formalism with numerous applications in artificial intelligence. ...

This paper studies a combined system of intuitionistic and classical propositional logic from proof-theoretic viewpoints. Based on the semantic treatment of Humberstone (J Philos Log 8:171–196, 1979) and del Cerro and Herzig (Frontiers of ...$\mathsf{}\mathbf{}\mathbf{}$$\mathsf{}\mathbf{}\mathbf{}$$\mathsf{}\mathbf{}\mathbf{}$$\mathbf{}\mathbf{}$

Matching logic (ML) is a formalism for specifying and reasoning about mathematical structures by means of patterns and pattern matching. Previously, it has been used to capture a number of other logics, e.g., separation logic with recursive ...

We provide a non-Gentzen, though fully syntactical, cut-elimination algorithm for classical propositional logic. The designed procedure is implemented on $\mathsf{GS}\mathsf{4}$, the one-sided version of Kleene’s sequent system $\mathsf{G}\mathsf{4}$. The algorithm here proposed proves ...$\mathsf{}\mathsf{}$

We introduce ill-founded sequent calculi for two intuitionistic linear-time temporal logics. Both logics are based on the language of intuitionistic propositional logic with ‘next’ and ‘until’ operators and are evaluated on dynamic Kripke models ...

Intuitionistic epistemic logic by Artemov and Protopopescu (Rev Symb Log 9:266–298, 2016) accepts the axiom “if A, then A is known” (written $A\supset KA$) in terms of the Brouwer–Heyting–Kolmogorov interpretation. There are two variants of intuitionistic ...$$$\mathbf{}$${\mathbf{}}^{}$

We develop infinitely many intuitionistic connexive logics with and which are obtained from intuitionistic propositional logic by adding the negation sign which admits principles of connexive implication and . We introduce -connexive logics ...

This paper provides a method to obtain terminating analytic calculi for a large class of intuitionistic modal logics. For a given logic L with a cut-free calculus G that is an extension of G3ip the method produces a terminating analytic calculus ...

We propose a minimal deontic logic, called MIND, based on intuitionistic logic. This logic gives a very simple solution to handling conflicting obligations: the presence of two conflicting obligations does not entail the triviality of the set of ...

This paper focuses on globally sound but possibly locally unsound analytic sequent calculi for quantifier macros defined by sequences of quantifiers. It is demonstrated that no locally sound analytic representation based on the usual ...

An inductive definition set (IDS, for short) of first-order predicate logic can be transformed into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent is valid w.r.t. the IDS if and only if a term equation ...

One proof-theoretic approach to equality in quantificational logic treats equality as a logical connective: in particular, term equality can be given both left and right introduction rules in a sequent calculus proof system. We present a ...

In Schwichtenberg (Studies in logic and the foundations of mathematics, vol 90, Elsevier, pp 867–895, 1977), Schwichtenberg fine-tuned Tait’s technique (Tait in The syntax and semantics of infinitary languages, Springer, pp 204–236, 1968) so as to ...

We present a sequent calculus with the Henkin constants in the place of the free variables. By disposing of the eigenvariable condition, we obtained a proof system with a strong locality property—the validity of each inference step depends only on ...

We present an axiomatization of the non-associative Lambek calculus extended with classical negation for which the frame semantics with the classical interpretation of negation is sound and complete.

This paper presents rules in sequent calculus for a binary quantifier I to formalise definite descriptions: Ix[F, G] means ‘The F is G’. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut ...

In this paper we construct a sequence of formulas $F_1,F_2,\dots$ with resolution proofs ${\pi }_1,{\pi }_2,\dots$ of these formulas after Andrews Skolemization, such that there is no elementary bound in the complexity of ${\pi }_1,{\pi }_2,\dots$ of resolution proofs ${\pi }_1^{\prime },{\pi }_2^{\prime },\dots$ after ...${\mathbf{}}^{}$$\mathbf{}$

Artemov and Protopopescu (2018) introduced a Brouwer-Heyting-Kolmogorov (BHK) interpretation of knowledge operator to define the intuitionistic epistemic logic IEL, where the axiom $A\supset KA$ is accepted but the axiom $KA\supset A$ is refused. This paper studies ...$\mathbf{}$