Some initial motivations for the Guarded Fragment still seem of interest in carrying its program further. First, we stress the equivalence between two perspectives: (a) satisfiability on standard models for guarded first-order formulas, and (b) satisfiability on general assignment models for arbitrary first-order formulas. In particular, we give a new straightforward reduction from the former notion to the latter. We also show how a perspective shift to general assignment models provides a new look at the fixed-point extension LFP(FO) of first-order (...) logic, making it decidable. Next, we relate guarded syntax to earlier quantifier restriction strategies for achieving effective axiomatizability in second-order logic – pointing at analogies with ‘persistent’ formulas, which are essentially in the Bounded Fragment of many-sorted first-order logic. Finally, we look at some further unexplored directions, including the systematic use of ‘quasi-models’ as a semantics by itself. (shrink)

We prove ExpTime-membership of the satisfiability problem for loosely ∀-guarded first-order formulas with a bounded number of variables and an unbounded number of constants. Guarded fragments with constants are interesting by themselves and because of their connection to hybrid logic.

By a fragment of a natural language we mean a subset of thatlanguage equipped with semantics which translate its sentences intosome formal system such as first-order logic. The familiar conceptsof satisfiability and entailment can be defined for anysuch fragment in a natural way. The question therefore arises, for anygiven fragment of a natural language, as to the computational complexityof determining satisfiability and entailment within that fragment. Wepresent a series of fragments of English for which the satisfiabilityproblem is polynomial, NP-complete, EXPTIME-complete,NEXPTIME-complete (...) and undecidable. Thus, this paper represents a casestudy in how to approach the problem of determining the logicalcomplexity of various natural language constructions. In addition, wedraw some general conclusions about the relationship between naturallanguage and formal logic. (shrink)

Controlled languages are regimented fragments of natural languagedesigned to make the processing of natural language more efficient andreliable. This paper defines a controlled language, E2V, whose principalgrammatical resources include determiners, relative clauses, reflexivesand pronouns. We provide a formal syntax and semantics for E2V, in whichanaphoric ambiguities are resolved in a linguistically natural way. Weshow that the expressive power of E2V is equal to that of thetwo-variable fragment of first-order logic. It follows that the problemof determining the satisfiability of a set (...) of E2V sentences is NEXPTIMEcomplete. We show that E2V can be extended in various ways withoutcompromising these complexity results; however, relaxing our policy onanaphora resolution renders the satisfiability problem for E2Vundecidable. Finally, we argue that our results have a bearing on thebroader philosophical issue of the relationship between natural andformal languages. (shrink)

Abstract State Machines (ASMs) provide a formal method for transparent design and specification of complex dynamic systems. They combine advantages of informal and formal methods. Applications of this method motivate a number of computability and decidability problems connected to ASMs. Such problems result for example from the area of verifying properties of ASMs. Their high expressive power leads rather directly to undecidability respectively uncomputability results for most interesting problems in the case of unrestricted ASMs. Consequently, it is rather natural to (...) ask whether there exist expressive classes of ASMs for which we can prove positive decidability and computability results. In this work, we introduce such a class of ASMs. The concept is similar to the one of the guarded fragment of first-order logic. We analyze the expressive power of this class and prove that it is stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. Some decidability and computability results have been proven in earlier works. (shrink)

We expand first order models with a tolerance relation on thedomain. Intuitively, two elements stand in this relation if they arecognitively close for the agent who holds the model. This simplenotion turns out to be very powerful. It leads to a semanticcharacterization of the guarded fragment of Andréka, van Benthemand Németi, and highlights the strong analogies between modallogic and this fragment. Viewing the resulting logic – tolerance logic– dynamically it is a resource-conscious information processingalternative to classical first order logic. The (...) differences areindicated by several examples. (shrink)

In the 1970s Codd introduced the relational algebra, with operators selection, projection, union, difference and product, and showed that it is equivalent to first-order logic. In this paper, we show that if we replace in Codd’s relational algebra the product operator by the “semijoin” operator, then the resulting “semijoin algebra” is equivalent to the guarded fragment of first-order logic. We also define a fixed point extension of the semijoin algebra that corresponds to μGF.

We show that the satisfiability problem for the monodic guarded, loosely guarded, and packed fragments of first-order temporal logic with equality is 2Exptime-complete for structures with arbitrary first-order domains, over linear time, dense linear time, rational number time, and some other classes of linear flows of time. We then show that for structures with finite first-order domains, these fragments are also 2Exptime-complete over real number time and hence over most of the commonly used linear flows of time, including the natural (...) numbers, integers, rationals, and any first-order definable class of linear flows of time. (shrink)

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, 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 GF2 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 GF2 without extra machinery such as fixed-point operators. (shrink)

We prove ExpTime-membership of the satisfiability problem for loosely ∀-guarded first-order formulas with a bounded number of variables and an unbounded number of constants. Guarded fragments with constants are interesting by themselves and because of their connection to hybrid logic.

ABSTRACT George Gargov was an active pioneer in the ‘Sofia School’ of modal logicians. Starting in the 1970s, he and his colleagues expanded the scope of the subject by introducing new modal expressive power, of various innovative kinds. The aim of this paper is to show some general patterns behind such extensions, and review some very general results that we know by now, 20 years later. We concentrate on simulation invariance, decidability, and correspondence. What seems clear is that ‘modal logic’ (...) as a genre of logical systems has a much wider scope than originally conceived, and that we have not reached its limits yet. (shrink)

This paper presents a simple decidable logic of functional dependence LFD, based on an extension of classical propositional logic with dependence atoms plus dependence quantifiers treated as modalities, within the setting of generalized assignment semantics for first order logic. The expressive strength, complete proof calculus and meta-properties of LFD are explored. Various language extensions are presented as well, up to undecidable modal-style logics for independence and dynamic logics of changing dependence models. Finally, more concrete settings for dependence are discussed: continuous (...) dependence in topological models, linear dependence in vector spaces, and temporal dependence in dynamical systems and games. (shrink)

This book illustrates the program of Logical-Informational Dynamics. Rational agents exploit the information available in the world in delicate ways, adopt a wide range of epistemic attitudes, and in that process, constantly change the world itself. Logical-Informational Dynamics is about logical systems putting such activities at center stage, focusing on the events by which we acquire information and change attitudes. Its contributions show many current logics of information and change at work, often in multi-agent settings where social behavior is essential, (...) and often stressing Johan van Benthem's pioneering work in establishing this program. However, this is not a Festschrift, but a rich tapestry for a field with a wealth of strands of its own. The reader will see the state of the art in such topics as information update, belief change, preference, learning over time, and strategic interaction in games. Moreover, no tight boundary has been enforced, and some chapters add more general mathematical or philosophical foundations or links to current trends in computer science. The theme of this book lies at the interface of many disciplines. Logic is the main methodology, but the various chapters cross easily between mathematics, computer science, philosophy, linguistics, cognitive and social sciences, while also ranging from pure theory to empirical work. Accordingly, the authors of this book represent a wide variety of original thinkers from different research communities. And their interconnected themes challenge at the same time how we think of logic, philosophy and computation. Thus, very much in line with van Benthem's work over many decades, the volume shows how all these disciplines form a natural unity in the perspective of dynamic logicians (broadly conceived) exploring their new themes today. And at the same time, in doing so, it offers a broader conception of logic with a certain grandeur, moving its horizons beyond the traditional study of consequence relations. (shrink)

This chapter presents a new semantics for inductive empirical knowledge. The epistemic agent is represented concretely as a learner who processes new inputs through time and who forms new beliefs from those inputs by means of a concrete, computable learning program. The agent’s belief state is represented hyper-intensionally as a set of time-indexed sentences. Knowledge is interpreted as avoidance of error in the limit and as having converged to true belief from the present time onward. Familiar topics are re-examined within (...) the semantics, such as inductive skepticism, the logic of discovery, Duhem’s problem, the articulation of theories by auxiliary hypotheses, the role of serendipity in scientific knowledge, Fitch’s paradox, deductive closure of knowability, whether one can know inductively that one knows inductively, whether one can know inductively that one does not know inductively, and whether expert instruction can spread common inductive knowledge—as opposed to mere, true belief—through a community of gullible pupils. (shrink)