In mathematical logic, a fragment of a logical language or theory is a subset of this logical language obtained by imposing syntactical restrictions on the language.[1] Hence, the well-formed formulae of the fragment are a subset of those in the original logic. However, the semantics of the formulae in the fragment and in the logic coincide, and any formula of the fragment can be expressed in the original logic.

The computational complexity of tasks such as satisfiability or model checking for the logical fragment can be no higher than the same tasks in the original logic, as there is a reduction from the first problem to the other. An important problem in computational logic is to determine fragments of well-known logics such as first-order logic that are as expressive as possible yet are decidable or more strongly have low computational complexity.[1] The field of descriptive complexity theory aims at establishing a link between logics and computational complexity theory, by identifying logical fragments that exactly capture certain complexity classes.[2]

References

  1. ^ a b Bradley, Aaron R.; Manna, Zohar (2007), The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, p. 70, ISBN 9783540741138.
  2. ^ Ebbinghaus, Heinz-Dieter; Flum, Jörg (2005), "Chapter 7. Descriptive Complexity Theory", Finite Model Theory, Perspectives in mathematical logic, Springer, pp. 119–164, ISBN 9783540287889.


Categories