Abstract Building on the small-model constructions for Åqvist’s deontic logics introduced in [24], we present Deo-SMT , an SMT-based reasoner implemented in Z3 for checking validity and generating countermodels. Deo-SMT covers all four of Åqvist’s logics ( E , F , F+(CM) , G ) and provides countermodel visualizations as text, matrices, and directed graphs. Our tool outperforms the existing Isabelle/HOL approach, while providing a lightweight and accessible interface for normative reasoning.

Normative Restraining Bolts (NRBs) adapt the restraining bolt technique (originally developed for safe reinforcement learning) to ensure compliance with social, legal, and ethical norms. While effective, NRBs rely on trial-and-error weight tuning, which hinders their ability to enforce hierarchical norms; moreover, norm updates require retraining. In this paper, we reformulate learning with NRBs as a multi-objective reinforcement learning (MORL) problem, where each norm is treated as a distinct objective. This enables the introduction of Ordered Normative Restraining Bolts (ONRBs), which support algorithmic weight selection, prioritized norms, norm updates, and provide formal guarantees on minimizing norm violations. Case studies show that ONRBs offer a robust and principled foundation for RL-agents to comply with a wide range of norms while achieving their goals.

The result model provides a foundation for precedent-based reasoning, yet real case bases are often inconsistent, with precedents pointing to opposite outcomes. To address this, we augment the result model with the Log-Odds Precedent Aggregator (LOPA)—a Naive-Bayes–style log-odds combiner that treats each applicable precedent as uncertain evidence, learns its reliability from data, and produces both a decision and a confidence score. We evaluate LOPA on the DIAS dataset, comparing it against other extensions of the result model, and a strong machine-learning baseline. Results show that the symbolic and hybrid models perform on par with ML, and in several settings slightly better, while remaining fully interpretable. LOPA is especially robust when many weak precedents compete with a few strong ones, and its calibrated confidence supports coverage–reliability tradeoffs.

Abstract The first algorithm to transform a proof in Nishimura’s sequent calculus $$\textbf{GKt}$$ GKt for tense logic $$\textbf{Kt}$$ Kt into an analytic proof of the same sequent is presented. In an analytic proof, every rule instance is analytic i.e., each formula in every premise is a subformula of some formula in its conclusion. We call this algorithm analytic restriction to convey that it extends analytic cut-restriction where just the cut-rule instances are made analytic. This distinction is essential in tense logic since cut and modal rules can both cause non-analyticity. Analytic cut-restriction is itself an extension of cut-elimination so our work contributes to a broader program of transforming arbitrary sequent proofs into ones constructed from a designated set of formulas—not necessarily subformulas. As with cut-elimination, the aim is to limit the proof search space and support proof-theoretic and meta-logical investigations.

Abstract Enhancing cut-free expressiveness through minimal structural additions to sequent calculus is a natural step. We focus on Åqvist’s system $$\textbf{F}$$ F with cautious monotonicity (CM), a deontic logic extension of $$\textbf{S5}$$ S 5 , for which we define a sequent calculus employing (semi) analytic cuts.The transition to hypersequents is key to develop modular and cut-free calculi for $$\mathbf{F + (CM)}$$ F + ( CM ) and $$\textbf{G}$$ G , also supporting countermodel construction.

We modify the restraining bolt technique, originally designed for safe reinforcement learning, to regulate agent behavior in alignment with social, ethical, and legal norms. Rather than maximizing rewards for norm compliance, our approach minimizes penalties for norm violations. We demonstrate in case studies the effectiveness of our approach in capturing benchmark challenges in normative reasoning like contrary-to-duty obligations, exceptions, and temporal obligations.

We introduce modular calculi for the logics for nonmonotonic reasoning defined by Kraus, Lehmann, and Magidor, featuring a strengthened form of analyticity. Our calculi are used to determine the computational complexity for the logics C, CL, CM, P (and M), and fragments thereof. The calculi are encoded into SMT solvers, yielding an efficient prover with countermodel generation capabilities. Our work encompasses known results and introduces new findings, including co-NP-completeness and a more effective semantics for C.

Although permissions are of crucial importance in several settings, they have garnered less attention within the deontic logic community than obligations. In previous work we showed how to reconstruct deontic logic using Kelsen’s quasi-causal conception of norms, restricting ourselves to the notion of obligation. Here we extend the account to permission, and show how to analyse the notion of strong permission through a Kelsenian lens. In our framework various forms of conflicts between obligation and permission are disentangled.

Input/Output (I/O) logic is a general framework for reasoning about conditional norms and/or causal relations. We streamline Bochman’s causal I/O logics via proof-search-oriented sequent calculi. Our calculi establish a natural syntactic link between the derivability in these logics and in the original I/O logics. As a consequence of our results, we obtain new, simple semantics for all these logics, complexity bounds, embeddings into normal modal logics, and efficient deduction methods. Our work encompasses many scattered results and provides uniform solutions to various unresolved problems.

Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations into decidability, complexity, disjunction property, interpolation, and more. Unfortunately cut-elimination does not hold for the sequent calculi of most non-classical logics. It is well-known that the key to applications is the subformula property (a typical consequence of cut-elimination) rather than cut-elimination itself. With this in mind, we introduce cut-restriction, a procedure to restrict arbitrary cuts to analytic cuts (when elimination is not possible). The algorithm applies to all sequent calculi satisfying language-independent and simple-to-check conditions, and it is obtained by adapting age-old cut-elimination. Our work encompasses existing results in a uniform way, subsumes Gentzen’s cut-elimination, and establishes new analytic cut properties.

Abstract We introduce a modular and transparent approach for augmenting the ability of reinforcement learning agents to comply with a given norm base. The normative supervisor module functions as both an event recorder and real-time compliance checker w.r.t. an external norm base. We have implemented this module with a theorem prover for defeasible deontic logic, in a reinforcement learning agent that we task with playing a “vegan” version of the arcade game Pac-Man.

Inspired by Kelsen’s view that norms establish causal-like connections between facts and sanctions, we develop a deontic logic in which a proposition is obligatory iff its complement causes a violation. We provide a logic for normative causality, define non-contextual and contextual notions of illicit and duty, and show that the logic of such duties is well-behaved and solves the main deontic paradoxes.

Abstract A sequent calculus with the subformula property has long been recognised as a highly favourable starting point for the proof theoretic investigation of a logic. However, most logics of interest cannot be presented using a sequent calculus with the subformula property. In response, many formalisms more intricate than the sequent calculus have been formulated. In this work we identify an alternative: retain the sequent calculus but generalise the subformula property to permit specific axiom substitutions and their subformulas. Our investigation leads to a classification of generalised subformula properties and is applied to infinitely many substructural, intermediate, and modal logics (specifically: those with a cut-free hypersequent calculus). We also develop a complementary perspective on the generalised subformula properties in terms of logical embeddings. This yields new complexity upper bounds for contractive-mingle substructural logics and situates isolated results on the so-called simple substitution property within a general theory.

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics.

We introduce a Curry–Howard correspondence for a large class of intermediate logics characterized by intuitionistic proofs with non-nested applications of rules for classical disjunctive tautologies (1-depth intermediate proofs). The resulting calculus, we call it λ∥, is a strongly normalizing parallel extension of the simply typed λ-calculus. Although simple, the λ∥ reduction rules can model arbitrary process network topologies, and encode interesting parallel programs ranging from numeric computation to algorithms on graphs.

We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such systems, and a rewriting of hypersequent rules as natural deduction rules.

We provide a standard completeness proof which uniformly applies to a large class of axiomatic extensions of Involutive Monoidal T-norm Logic (IMTL). In particular, we identify sufficient conditions on the proof calculi which ensure density elimination and then standard completeness. Our argument contrasts with all previous approaches for involutive logics which are logic-specific.

Propositional Gödel logic G extends intuitionistic logic with the non-constructive principle of linearity (A → B) ∨ (B → A). We introduce a Curry-Howard correspondence for G and show that a simple natural deduction calculus can be used as a typing system. The resulting functional language extends the simply typed λ-calculus via a synchronous communication mechanism between parallel processes, which increases its expressive power. The normalization proof employs original termination arguments and proof transformations implementing forms of code mobility. Our results provide a computational interpretation of G, thus proving A. Avron's 1991 thesis.

We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure. A general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions is then proved. We adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus DFLe and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.

This volume contains selected papers from the workshop ‘Concepts and Meaning’ held on 2–5 May 2012 at the Vienna University of Technology in honour of the 60th birthday of Alexander Leitsch. Alexander Leitsch made substantial contributions to a variety of different research areas including automated deduction, computability theory, proof theory and formal mathematics. The broad scope of his research interests is reflected in the contents of this special issue that features the following papers (in alphabetic order): ... A common thread that runs through Alexander Leitsch' scientific work is his mastery of syntactic precision rooted in the conviction that the syntactic form not only captures but even determines the semantic meaning of concepts, hence also the title of this special issue. In addition to his scientific activities he is also an inspiring colleague and a dedicated and enthusiastic teacher as witnessed by generations of his students who are now successful in academia as well as in industry, some of which are represented in this volume.

The possession of a suitable proof-calculus is the starting point for many investigations into a logic, including decidability and complexity, computational interpretations and automated theorem proving. By suitable proof-calculus we mean a calculus whose proofs exhibit some notion of subformula property ("analyticity"). In this talk we describe a method for the algorithmic introduction of analytic sequent-style calculi for a wide range of non-classical logics starting from Hilbert systems. To demonstrate the widespread applicability of this method, we discuss how to use the introduced calculi for proving various results ranging from Curry-Howard isomorphism to new interpretative tools for Indology.

We introduce a first sequent-style calculus for witnessed Gödel logic. Our calculus makes use of the cut rule. We show that this is inescapable by establishing a general result on the non-existence of suitable analytic calculi for a large class of first-order logics. These include witnessed Gödel logic, (fragments of) Łukasiewicz logic and intuitionistic logic extended with the quantifiers of classical logic.

What can (and cannot) be expressed by structural display rules? Given a display calculus, we present a systematic procedure for transforming axioms into structural rules. The conditions for the procedure are given in terms of (purely syntactic) abstract properties of the base calculus; thus, the method applies to large classes of calculi and logics. If the calculus satisfies certain additional properties, we prove the converse direction, thus characterising the class of axioms that can be captured by structural display rules. Determining if an axiom belongs to this class or not is shown to be decidable. Applied to the display calculus for tense logic, we obtain a new proof of Kracht’s Display Theorem I.

We develop a fully algorithmic approach to “taming” logics expressed Hilbert style, that is, reformulating them in terms of analytic sequent calculi and useful semantics. Our approach applies to Hilbert calculi extending the positive fragment of propositional classical logic with axioms of a certain general form that contain new unary connectives. Our work encompasses various results already obtained for specific logics. It can be applied to new logics, as well as to known logics for which an analytic calculus or a useful semantics has so far not been available. A Prolog implementation of the method is described.

federated and organized in parallel by Masaryk University in Brno, Czech Republic.The MFCS symposia, organized since 1972, encourage high-quality research in all branches of theoretical computer science.The broad scope of MFCS provides an opportunity to bring together researchers who do not usually meet at specialized conferences.Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL).The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science.

We extend the methodology in Baaz and Fermüller (1999) [5] to systematically construct analytic calculi for semi-projective logics-a large family of (propositional) locally finite many-valued logics. Our calculi, defined in the framework of sequents of relations, are proof search oriented and can be used to settle the computational complexity of the formalized logics. As a case study we derive sequent calculi of relations for Nilpotent Minimum logic and for Hajek's Basic Logic extended with the [Formula: see text]-contraction axiom ([Formula: see text]). The introduced calculi are used to prove that the decidability problem in these logics is Co-NP complete.

We introduce a systematic procedure to transform large classes of (Hilbert) axioms into equivalent inference rules in sequent and hypersequent calculi. This allows for the automated generation of analytic calculi for a wide range of prepositional nonclassical logics including intermediate, fuzzy and substructural logics. Our work encompasses many existing results, allows for the definition of new calculi and contains a uniform semantic proof of cut-elimination for hypersequent calculi.

We investigate cut elimination in propositional substructural logics. The problem is to decide whether a given calculus admits (reductive) cut elimination. We show that for commutative single-conclusion sequent calculi containing generalised knotted structural rules and arbitrary logical rules the problem can be decided by resolution-based methods. A general cut-elimination proof for these calculi is also provided.

Hypersequent calculi arise by generalizing standard sequent calculi to refer to whole contexts of sequents instead of single sequents. We present a number of results using hypersequents to obtain a Gentzen-style characterization for the family of Gödel logics. We first describe analytic calculi for propositional finite and infinite-valued Gödel logics. We then show that the framework of hypersequents allows one to move straightforwardly from the propositional level to first-order as well as propositional quantification. A certain type of modality, enhancing the expressive power of Gödel logic, is also considered.

In this paper we define cut‐free hypersequent calculi for some intermediate logics semantically characterized by bounded Kripke models. In particular we consider the logics characterized by Kripke models of bounded width Bwk, by Kripke models of bounded cardinality Bck and by linearly ordered Kripke models of bounded cardinality Gk. The latter family of logics coincides with finite‐valued Gödel logics. Our calculi turn out to be very simple and natural. Indeed, for each family of logics (respectively, Bwk, Bck and Gk), they are defined by adding just one structural rule to a common system, namely the hypersequent calculus for Intuitionistic Logic. This structural rule reflects in a natural way the characteristic semantical features of the corresponding logic.

In this paper we define internal cut-free sequent calculi for any n-valued Lukasiewicz logic Ln. These calculi are based on a representation of formulas of Ln, by n - 1 many {0, 1}-valued formulas of Ln. They enjoy the usual properties of sequent systems like symmetry, subformula property and invertibility of the rules. Upon dualizing our calculi one obtains Hähnle's tableau systems. Then they provide a reformulation of Hähnle's approach to theorem proving that makes no use of nonlogical elements.

Abstract A Partial Combinatory Algebra is completable if it can be extended to a total one. In [1] it is asked (question 11, posed by D. Scott, H. Barendregt, and G. Mitschke) if every PCA can be completed. A negative answer to this question was given by Klop in [12, 11]; moreover he provided a sufficient condition for completability of a PCA (M, •, K,S) in the form of ten axioms (inequalities) on terms of M. We prove that just one of these axiom (the so called Barendregt's axiom) is sufficient to guarantee (a slightly weaker notion of) completability.