# Modal Languages and Bounded Fragments of Predicate Logic

@article{Andrka1998ModalLA, title={Modal Languages and Bounded Fragments of Predicate Logic}, author={Hajnal Andr{\'e}ka and Istv{\'a}n N{\'e}meti and Johan van Benthem}, journal={Journal of Philosophical Logic}, year={1998}, volume={27}, pages={217-274} }

Definition des fragments modaux de la logique des predicats a partir de formules du premier ordre qui sont des traductions des proprietes poly-modales elementaires. Distinguant les fragments variables et finis des fragments lies a un quantificateur, l'A. developpe une version semantique des fragments gardes en remplacant les liens syntaxiques par des restrictions sur les types d'attribution dans les modeles generalises. Se referant a l'algebre cylindrique, l'A. indique les nouvelles directions… Expand

#### Topics from this paper

#### 629 Citations

Description Logics and the Two-Variable Fragment

- Computer Science
- Description Logics
- 2001

It is proved that L has the same expressive power as the two-variable fragment FO 2 of rst-order logi by presenting a translation from FO 2 -formulae into equivalent Lon epts (and ba k). Expand

Sequent Systems for Modal Logics

- Computer Science
- 2002

This chapter surveys the application of various kinds of sequent systems to modal and temporal logic, also called tense logic, using ordinary Gentzen sequents as a starting point. Expand

Modal Logic and the Two-Variable Fragment

- Mathematics, Computer Science
- CSL
- 2001

It is proved that L has the same expressive power as the two-variable fragment FO^2 of first-order logic but speaks less succinctly about relational structures: if the number of relations is bounded, then L-satisfiability is Exp time-complete but FO^1 satisfiability is NExpTime-complete. Expand

Hybrid logic is the bounded fragment of first order logic.

- Mathematics
- 1999

Hybrid languages are extended modal languages which can refer to (or even quantify over) worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work (for example [BS98,… Expand

SOME MODEL THEORY OF GUARDED NEGATION

- Mathematics, Computer Science
- The Journal of Symbolic Logic
- 2018

Results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics. Expand

Modal Logic and the two-variable fragment ( Revised Version )

- 2019

We introduce a modal language L which is obtained from standard modal logic by adding the Boolean operators on accessibility relations, the identity relation, and the converse of relations. It is… Expand

Algorithmic correspondence and completeness in modal logic

- Mathematics, Computer Science
- J. Appl. Non Class. Logics
- 2008

This paper develops several extensions of SQEMA where that syntactic condition is replaced by a semantic one, viz. downward monotonicity, and proves correctness for a large class of modal formulae containing an extension of the Sahlqvist formULae, defined by replacing polarity with monotonic. Expand

Decidability Frontier for Fragments of First-Order Logic with Transitivity

- Mathematics, Computer Science
- Description Logics
- 2018

This talk surveys results concerning the decidability frontier of the decidable fragments of first-order logic extended with transitivity, and discusses both, general and finite satisfiability, as presence of transitivity axioms often allows one to express axiomatic of infinity. Expand

Binding Forms in First-Order Logic

- Mathematics, Computer Science
- CSL
- 2015

A hierarchy of four fragments focused on the Boolean combinations of these forms is described, showing that the less expressive one is already incomparable with several first-order limitations proposed in the literature, as the guarded and unary negation fragments. Expand

Rewriting Guarded Negation Queries

- Computer Science
- MFCS
- 2013

This paper establishes that GNFO queries have distinctive features with respect to rewriting, and results include effective preservation theorems for GNFO, Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries withrespect to GNFO constraints within very restricted logics. Expand

#### References

SHOWING 1-10 OF 126 REFERENCES

A Modal Logic for Quantification and Substitution

- Mathematics, Computer Science
- Log. J. IGPL
- 1994

A modal formalism called cylindric mirror modal logic is defined, and it is shown how it is a modal version of first order logic with substitution, and a semantics is defined for the language which is closely related to algebraic logic as Polyadic Equality Algebras as the modal or complex algebra of this system. Expand

Semantics-Based Translation Methods for Modal Logics

- Mathematics
- 1991

A general framework for translating logical formulae from one logic into another logic is presented. The framework is instantiated with two different approaches to translating modal logic formulae… Expand

Modal Foundations for Predicate Logic

- Computer Science
- Log. J. IGPL
- 1997

This paper investigatèlighter' versions of this general purpose tool, by modally deconstructing the usual semantics, and locating implicit choice points in its set up, and providing technical elaborations demonstrating its viability. Expand

Back and Forth Between Modal Logic and Classical Logic

- Computer Science
- Log. J. IGPL
- 1995

This paper proves decidability for a largèbounded fragment' of predicate logic, and points out several applications, including a fresh look at the landscape of possible predicate logics, including candi-685. Expand

On a decidable generalized quantifier logic corresponding to a decidable fragment of first-order logic

- Mathematics, Computer Science
- J. Log. Lang. Inf.
- 1995

The logic ofQ (without ordinary quantifiers) corresponds therefore to the fragment of first-order logic which contains only specially restricted quantification and it is proved that it is decidable using the method of analytic tableaux. Expand

EXPRESSIVE FUNCTIONAL COMPLETENESS IN TENSE LOGIC

- Computer Science
- 1981

A propositional language with atomic propositions p, q, r, . . . the usual classical connectives ∼,∧,∨ → and some additional connectives denoted by various symbols such as |=, , etc is considered. Expand

Cylindric modal logic

- Mathematics, Medicine
- 1993

From this modal viewpoint, the standard semantics of first-order logic corresponds to just one of many possible classes of Kripke frames, and that other classes might be of interest as well. Expand

Relational queries computable in polynomial time (Extended Abstract)

- Computer Science
- STOC '82
- 1982

This paper shows that the Fixpoint Hierarchy collapses at the first fixpoint level, and shows weaker languages for expressing less complex queries, and gives a simple syntactic categorization of those queries which can be answered in polynomial time. Expand

Logic of transition systems

- Mathematics, Computer Science
- J. Log. Lang. Inf.
- 1994

This paper shows how labeled transition systems lend themselves to ordinary logical analysis (without any special new formalisms), by introducing their standard first-order theory, and hopes that this puts standard logical formalisms on the map as a serious option for a theory of computational processes. Expand

Generalized quantifiers and pebble games on finite structures

- Mathematics, Computer Science
- [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science
- 1992

It is shown that equivalence of finite structures relative to the new logics can be characterized in terms of certain pebble games that are a variant of the Ehrenfeucht-Fraisse games. Expand