Finite model property

Finite model property

In logic, we say a logic L has the finite model property (fmp for short) if there is a class of models M of L (i.e. each model M is a model of L) such that any non-theorem of L is falsified by some "finite" model in M. Another way of putting this is to say that L has the fmp if for every formula A of L, A is an L-theorem iff A is a theorem of the theory of finite models of L.

If L is finitely axiomatizable (and has a recursive set of recursive rules) and has the fmp, then it is decidable.

References

Blackburn P., de Rijke M., Venema Y. "Modal Logic". Cambridge University Press, 2001.


Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Finite model theory — is a subfield of model theory that focuses on properties of logical languages, such as first order logic, over finite structures, such as finite groups, graphs, databases, and most abstract machines. It focuses in particular on connections… …   Wikipedia

  • Model theory — This article is about the mathematical discipline. For the informal notion in other parts of mathematics and science, see Mathematical model. In mathematics, model theory is the study of (classes of) mathematical structures (e.g. groups, fields,… …   Wikipedia

  • Model-based testing — is the application of Model based design for designing and optionally executing the necessary artifacts to perform software testing. Models can be used to represent the desired behavior of the System Under Test (SUT), or to represent the desired… …   Wikipedia

  • Model checking — This article is about checking of models in computer science. For the checking of models in statistics, see regression model validation. In computer science, model checking refers to the following problem: Given a model of a system, test… …   Wikipedia

  • Finite & Deterministic Discrete Event System Specification — FD DEVS (Finite Deterministic Discrete Event System Specification) is a formalism for modeling and analyzing discrete event dynamic systems in both simulation and verification ways. FD DEVS also provides modular and hierarchical modeling features …   Wikipedia

  • Denotational semantics of the Actor model — The denotational semantics of the Actor model is the subject of denotational domain theory for Actors. The historical development of this subject is recounted in [Hewitt 2008b]. Contents 1 Actor fixed point semantics 2 Compositionality in… …   Wikipedia

  • Temporal logic in finite-state verification — In finite state verification, model checkers examine finite state machines representing concurrent software systems looking for errors in design. Errors are defined as violations of requirements expressed as properties of the system. In the event …   Wikipedia

  • Stable model semantics — The concept of a stable model, or answer set, is used to define a declarative semantics for logic programs with negation as failure. This is one of several standard approaches to the meaning of negation in logic programming, along with program… …   Wikipedia

  • Actor model — In computer science, the Actor model is a mathematical model of concurrent computation that treats actors as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions …   Wikipedia

  • NIP (model theory) — In model theory, a branch of mathematical logic, a complete theory T is said to satisfy NIP (or not the independence property ) if none of its formulae satisfy the independence property, that is if none of its formulae can pick out any given… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”