Analytic Calculi for Logics of Ordinal Multiples of Standard t-Norms

For two propositional fuzzy logics, we present analytic proofcalculi, based on relational hypersequents. The logic consideredfirst, called M, is based on the finite ordinal sums of ukasiewiczt-norms. In addition to the usual connectives—the conjunction, the implication and the constant 0—we use a furtherunary connective interpreted by the function associating witheach truth value a the greatest -idempotent below a. M is aconservative extension of Basic Logic. The second logic, called M, is based on the finite ordinal sumsof the product t-norm on (0, 1]. Our connectives are in thiscase just the conjunction and the implication.     

Logic of Proofs and Labels with a Complete Set of Operations

We develop a framework in which operations on proofs can bespecified and studied. Proofs are treated as structures builtfrom atomic proofs and references by means of computable operations. Our approach extends the ideas of Logic of Proofs (Artemov,1995, Bull. Symb. Logic, 7, 1–36) in which the proof predicate‘t is a proof of F ’ is incorporated into the propositionallanguage. We introduce an additional storage predicate ‘xis a label for F ’ (Yavorskaya, 2005, J. Logic Comput.,15, 517–537). In this article which is essentially a continuation of Yavorskaya'swork, we study a natural example of a logic with operationson proofs and labels. This logic is decidable and complete with respect to its intended semantics. is capable to internalizeits own proofs, and operations of suffice to realize all operations specified in the languagewith proofs and labels.     

Using Resolution for Testing Modal Satisfiability and Building Models

This paper presents a translation-based resolution decision procedure for the multimodal logic K _(m)(,,) defined over families of relations closed under intersection, union, and converse. The relations may satisfy certain additional frame properties. Different from previous resolution decision procedures that are based on ordering refinements, our procedure is based on a selection refinement, the derivations of which correspond to derivations of tableaux or sequent proof systems. This procedure has the advantage that it can be used both as a satisfiability checker and as a model builder. We show that tableaux and sequent-style proof systems can be polynomially simulated with our procedure. Furthermore, the finite model property follows for a number of extended modal logics.     

Reference Constructions in the Single-conclusion Proof Logic

We propose an extension of the propositional proof logic languageby the second-order variables denoting the reference constructors(like ‘the formula which is proven by x’). The prooflogic in this weak second-order language is axiomatized viathe calculus _ref, the (Functional)Logic of Proofs with References. It is supplied with the formalarithmetical semantics: we prove that _ref is sound with respect to arithmetical interpretationsand is a conservative extension of propositional single-conclusionproof logic . Finally,we demonstrate how the language of _ref can be used as a scheme language for arithmetic and providethe corresponding proof conversion method.     

Embedding Alternating-time Temporal Logic in Strategic Logic of Agency

Seeing To It That ()logic is a logic of agency, proposed in the 1990s in the domainof philosophy of action. It is the logic of constructions ofthe form ‘agent a sees to it that ’. We believethat theory can contributeto the logical analysis of multiagent systems. To support thisclaim, we show that there is a close relationship with morerecent logics for multiagent systems. This work extends Broersenet al. (2006, Electron Notes Theor. Comput. Sci., Vol. 157,pp. 23–35) where we presented a translation from Pauly'sCoalition Logic to Chellas' logic. Here we focus on Alur, Henzinger and Kupferman's Alternating-timeTemporal Logic , andthe logic of the ‘fused’ _s[_scstit : _] operatorfor strategic ability, as described by Horty. After a briefpresentation of ATL and the definition of a discrete-time strategic framework slightly adaptedfrom Horty, we give a translation from ATL to the framework, and prove that it determines correctembedding.     

A polynomial space construction of tree-like models for logics with local chains of modal connectives

The LA-logics (“logics with Local Agreement”) are polymodal logics defined semantically such that at any world of a model, the sets of successors for the different accessibility relations can be linearly ordered and the accessibility relations are equivalence relations. In a previous work, we have shown that every LA-logic defined with a finite set of modal indices has an NP-complete satisfiability problem. In this paper, we introduce a class of LA-logics with a countably infinite set of modal indices and we show that the satisfiability problem is PSPACE-complete for every logic of such a class. The upper bound is shown by exhibiting a tree structure of the models. This allows us to establish a surprising correspondence between the modal depth of formulae and the number of occurrences of distinct modal connectives. More importantly, as a consequence, we can show the PSPACE-completeness of Gargov's logic DALLA and Nakamura's logic LGM restricted to modal indices that are rational numbers, for which the computational complexity characterization has been open until now. These logics are known to belong to the class of information logics and fuzzy modal logics, respectively.     

In All But Finitely Many Possible Worlds: Model-Theoretic Investigations on ‘<Emphasis Type="Italic">Overwhelming Majority</Emphasis>’ Default Conditionals

Defeasible conditionals are statements of the form ‘if A then normally B’. One plausible interpretation introduced in nonmonotonic reasoning dictates that (\(A\Rightarrow B\)) is true iff B is true in ‘most’ A-worlds. In this paper, we investigate defeasible conditionals constructed upon a notion of ‘overwhelming majority’, defined as ‘truth in a cofinite subset of \(\omega \)’, the first infinite ordinal. One approach employs the modal logic of the frame \((\omega , <)\), used in the temporal logic of discrete linear time. We introduce and investigate conditionals, defined modally over \((\omega , <)\); several modal definitions of the conditional connective are examined, with an emphasis on the nonmonotonic ones. An alternative interpretation of ‘majority’ as sets cofinal (in \(\omega \)) rather than cofinite (subsets of \(\omega \)) is examined. For these modal approaches over \((\omega , <)\), a decision procedure readily emerges, as the modal logic \({\mathbf {K4DLZ}}\) of this frame is well-known and a translation of the conditional sentences can be mechanically checked for validity; this allows also for a quick proof of \(\mathsf {NP}\)-completeness of the satisfiability problem for these logics. A second approach employs the conditional version of Scott-Montague semantics, in the form of \(\omega \)-many possible worlds, endowed with neighborhoods populated by collections of cofinite subsets of \(\omega \). This approach gives rise to weak conditional logics, as expected. The relative strength of the conditionals introduced is compared to (the conditional logic ‘equivalent’ of) KLM logics and other conditional logics in the literature.     

The consistency of syntactical treatments of knowledge1 (How to compile quantificational modal logics into classical FOL)

The relative expressive power of a sentential operator □α is compared to that of a syntactical predicate L(‘α’) in the setting of first-order logics. Despite well-known results by Montague and by Thomason that claim otherwise, any of the so-called “modal” logics of knowledge and belief can be compiled into classical first-order logics that have a corresponding predicate on sentences. Moreover, through the use of a partial truth predicate, the standard modal axiom schemata can be translated into single sentences, making it possible to use conventional first-order logic theorem provers to directly derive results in a wide class of modal logics.     

Prehistoric Graph in Modal Derivations and Self-Referentiality

By terms-allowed-in-formulas capacity, Artemov’s Logic of Proofs LP Artemov includes self-referential formulas of the form t:?(t) that play a crucial role in the realization of modal logic S4 in LP, and in the Brouwer–Heyting–Kolmogorov semantics of intuitionistic logic via LP. In an earlier work appeared in the Proceedings of CSR 2010 the author defined prehistoric loop in a sequent calculus of S4, and verified its necessity to self-referentiality in S4?LP realization. In this extended version we generalize results there to T and K4, two modal logics smaller than S4 that yet call for self-referentiality in their realizations into corresponding justification logics JT and J4.     

The complexity of constraint satisfaction problems for small relation algebras

Andréka and Maddux [Notre Dame J. Formal Logic 35 (4) 1994] classified the small relation algebras—those with at most 8 elements, or in other terms, at most 3 atomic relations. They showed that there are eighteen isomorphism types of small relation algebras, all representable. For each simple, small relation algebra they computed the spectrum of the algebra, namely the set of cardinalities of square representations of that relation algebra.In this paper we analyze the computational complexity of the problem of deciding the satisfiability of a finite set of constraints built on any small relation algebra. We give a complete classification of the complexities of the general constraint satisfaction problem for small relation algebras. For three of the small relation algebras the constraint satisfaction problem is NP-complete, for the other fifteen small relation algebras the constraint satisfaction problem has cubic (or lower) complexity.We also classify the complexity of the constraint satisfaction problem over fixed finite representations of any relation algebra. If the representation has size two or less then the complexity is cubic (or lower), but if the representation is square, finite and bigger than two then the complexity is NP-complete.     

Computability in Specification

In reference (Foundation of specification. Journal of Logicand Computation, 15, 951–974, 2005), the author introducesa core specification theory (CST) in order to provide a logicalframework for the design and exploration of specification languages.In this article, we formulate two highly expressive extensionsof CST. The first (CST_U) is CST + a universe of types and thesecond (CST_US) permits specifications themselves to be dataitems. Finally, we shall explore their metamathematical propertiesand, in particular, provide an interpretation into first-orderarithmetic.     

Deciding Regular Grammar Logics with Converse Through First-Order Logic

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF², which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF² include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF² without extra machinery such as fixed-point operators.     

The Difference between Polynomial-Time Many-One and Truth-Table Reducibilities on Distributional Problems

In this paper we separate many-one reducibility from truth-table reducibility for distributional problems in DistNP under the hypothesis that P ≠ NP . As a first example we consider the 3-Satisfiability problem (3SAT) with two different distributions on 3CNF formulas. We show that 3SAT with a version of the standard distribution is truth-table reducible but not many-one reducible to 3SAT with a less redundant distribution unless P = NP . We extend this separation result and define a distributional complexity class C with the following properties: (1) C is a subclass of DistNP, this relation is proper unless P = NP. (2) C contains DistP, but it is not contained in AveP unless DistNP \subseteq AveZPP. (3) C has a ≤ ^p _m -complete set. (4) C has a ≤ ^p _tt -complete set that is not ≤ ^p _m -complete unless P = NP. This shows that under the assumption that P ≠ NP, the two completeness notions differ on some nontrivial subclass of DistNP.     

Branching-Time Logics Repeatedly Referring to States

While classical temporal logics lose track of a state as soon as a temporal operator is applied, several branching-time logics able to repeatedly refer to a state have been introduced in the literature. We study such logics by introducing a new formalism, hybrid branching-time logics, subsuming the other approaches and making the ability to refer to a state more explicit by assigning a name to it. We analyze the expressive power of hybrid branching-time logics and the complexity of their satisfiability problem. As main result, the satisfiability problem for the hybrid versions of several branching-time logics is proved to be 2EXPTIME-complete. To prove the upper bound, the automata-theoretic approach to branching-time logics is extended to hybrid logics. As a result of independent interest, the nonemptiness problem for alternating one-pebble Büchi tree automata is shown to be 2EXPTIME-complete. A common property of the logics studied is that they refer to only one state. This restriction is crucial: The ability to refer to more than one state causes a nonelementary blow-up in complexity. In particular, we prove that satisfiability for NCTL* has nonelementary complexity.     

Justification logics, logics of knowledge, and conservativity

Several justification logics have been created, starting with the logic LP, (Artemov, Bull Symbolic Logic 7(1):1–36, 2001). These can be thought of as explicit versions of modal logics, or of logics of knowledge or belief, in which the unanalyzed necessity (knowledge, belief) operator has been replaced with a family of explicit justification terms. We begin by sketching the basics of justification logics and their relations with modal logics. Then we move to new material. Modal logics come in various strengths. For their corresponding justification logics, differing strength is reflected in different vocabularies. What we show here is that for justification logics corresponding to modal logics extending T, various familiar extensions are actually conservative with respect to each other. Our method of proof is very simple, and general enough to handle several justification logics not directly corresponding to distinct modal logics. Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend T. That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open.     

Power indices and easier hard problems

The concepts of power_index, satisfiability hypothesis (SH), and structure tree are introduced and used to make sharper hypotheses about a problem's complexity than the problem isNP-complete. These concepts are used to characterize the complexities of a number of basicNP-complete problems, including both CLIQUE and PARTITION which are shown to have power-indices at most 1/2. Also, the problem 3SAT is shown to be solvable deterministically in time exponential only in thesquare root ofv+c, wherev is the number of variables andc is the number of crossovers needed to layout the formula in the plane.The research of R. E. Stearns was supported by NSF Grants DCR 83-03932 and CCR 89-03319, and that of H. B. Hunt was supported by NSF Grants DCR 86-03184 and CCR 89-03319.     

Eliminability of cut in hypersequent calculi for some modal logics of linear frames

Hypersequent calculi, introduced independently by Pottinger and Avron, provide a powerful generalization of ordinary sequent calculi. In the paper we present a proof of eliminability of cut in hypersequent calculi for three modal logics of linear frames: K4.3, KD4.3 and S4.3. Our cut-free calculus is based on Avron's HC formalization for Gödel–Dummett's logic. The presented proof of eliminability of cut is purely syntactical and based on Ciabattoni, Metcalfe, Montagna's proof of eliminability of cut for hypersequent calculi for some fuzzy logics with modalities.     

Comparing variants of strategic ability: how uncertainty and memory influence general properties of games

Alternating-time temporal logic (ATL) is a modal logic that allows to reason about agents’ abilities in game-like scenarios. Semantic variants of ATL are usually built upon different assumptions about the kind of game that is played, including capabilities of agents (perfect vs. imperfect information, perfect vs. imperfect memory, etc.). ATL has been studied extensively in previous years; however, most of the research focused on model checking. Studies of other decision problems (e.g., satisfiability) and formal meta-properties of the logic (like axiomatization or expressivity) have been relatively scarce, and mostly limited to the basic variant of ATL where agents possess perfect information and perfect memory. In particular, a comparison between different semantic variants of the logic is largely left untouched. In this paper, we show that different semantics of ability in ATL give rise to different validity sets. The issue is important for several reasons. First, many logicians identify a logic with its set of true sentences. As a consequence, we prove that different notions of ability induce different strategic logics. Secondly, we show that different concepts of ability induce different general properties of games. Thirdly, the study can be seen as the first systematic step towards satisfiability-checking algorithms for ATL with imperfect information. We introduce sophisticated unfoldings of models and prove invariance results that are an important technical contribution to formal analysis of strategic logics.