We introduce a simple game of resource-conscious reasoning. In this two-player game, players P and O place tokens of positive and negative polarity onto a game board according to certain rules. P wins if she manages to match every negative token with a corresponding positive token. We study this token game using methods from computational complexity and proof theory. Specifically, we show complexity results for various fragments of the game, in- cluding PSPACE-completeness of a finite restriction and undecidability of the full game featuring non-terminating plays. Moreover, we show that the finitary version of the game is axiomatisable and can be embedded into exponential-free linear logic. The full game is shown to satisfy the exponential rules of linear logic, but is not fully captured by it. Finally, we show determinacy of the game, that is the existence of a winning strategy for one of the players.

Group polarization, the phenomenon where individuals become more extreme after in- teracting, has been gaining attention, especially with the rise of social media shaping peo- ple’s opinions. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this work we consider the modal logic PNL that captures the no- tion of agents agreeing or disagreeing on a given topic. Our contribution involves enhancing PNL with advanced formal reasoning techniques, instead of relying on axiomatic systems for analyzing group polarization. To achieve this, we introduce a semantic game tailored for (hybrid) extensions of PNL. This game fosters dynamic reasoning about concrete net- work models, aligning with our goal of strengthening PNL’s effectiveness in studying group polarization. We show how this semantic game leads to a provability game by systemically exploring the truth in all models. This leads to the first cut-free sequent systems for some variants of PNL. Using polarization of formulas, the proposed calculi can be modularly adapted to consider different frame properties of the underlying model.

We explore systematic connections between weighted (semi-abstract) argumentation frames and t-norm-based fuzzy logics. To this aim we introduce the concept of argumentative immunity, as well as corresponding notions of argumentative soundness and completeness with respect to given sets of logical attack principles. For Gödel logic, a detailed proof of argumentative soundness and completeness with respect to appropriate principles is presented. For Łukasiewicz and product logic this is indicated more briefly, but with some hints on corresponding interpretations of the attack relation between (claims of) arguments. Moreover, the central axiom of prelinearity is analyzed from our argumentation-based perspective.

Hintikka's semantic game for classical logic is generalized to the family of all finite-valued matrices. This in turn serves as a springboard for developing game semantics for all propositional formulas with respect to arbitrary finite non-deterministic matrices. In this approach a new concept of non-deterministic valuation, called ‘liberal valuation’, emerges that augments the usually employed static and dynamic valuations in a natural manner. Liberal valuation is shown to correspond to unrestricted semantic games, while the characterization of static and dynamic valuations involves certain restrictions of the game that are handled by an interactive pruning procedure.

The size of shortest cut-free proofs of first-order formulas in intuitionistic sequent calculus is known to be non-elementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cut-free proofs for disjunction-free intuitionistic logic for the case where the cut-formulas of the original proof are prenex. Moreover, we establish non-elementary lower bounds for classical disjunction-free proofs with prenex cut-formulas and intuitionistic disjunction-free proofs with non-prenex cut-formulas.

Journal Article Model Representation over Finite and Infinite Signatures Get access Christian G. Fermüller, Christian G. Fermüller Technische Universität Wien, A-1040 Vienna, Austria. Search for other works by this author on: Oxford Academic Google Scholar Reinhard Pichler Reinhard Pichler Technische Universität Wien, A-1040 Vienna, Austria. Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 17, Issue 3, June 2007, Pages 453–477, https://doi.org/10.1093/logcom/exm008 Published: 21 March 2007 Article history Received: 12 October 2006 Published: 21 March 2007

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.

Building on previous results that show that hyperresolution refinements may usefully be employed as decision proceduresfor a wide range of decidable classes of clause sets we present methods for constructing models for such sets of clauses. We show how to generate finite sets of atoms that respresent Herbrand models using hyperresolution. We demonstrate that these atomic representations of models enjoy features that provide a basis for various applications in automated theorem proving. In particular, we show that the equivalence of atomic representations is decidable and that arbitrary clauses can beevaluated effectively w.r.t. to the represented models. For the investigated classes we may focus on atoms with a linear term structure and show that, for this important subcase, finite models can be extracted from the sets of atoms generated by hyperresolution. We emphasize that, in contrast to model theoretic approaches, no backtracking is needed in our proof theoretic model constructing algorithm.

We investigate the effects of different types of translations of first-order formulas to clausal form on minimal proof length. We show that there is a sequence of unsatisfiable formulassuch that the length of all refutations of non-structural clause forms of F/sub n/ is non-elementary (in the size of F/sub n/), but there are refutations of structural clause forms of F/sub n/ that are of elementary (at most triple exponential) length.>