Next: Establishing Complexity Bounds
Up: Applications
Previous: Refutational Theorem Proving
Contents
Saturation of a Theory
When we are interested in the finite saturation of a theory,
we don't expect to find a contradiction and hence want to
limit forward computation as much as possible.
In that case certain meta-logical directives, including the reduction ordering,
have to be set manually.
Harald Ganzinger
2002-12-04
Imprint | Data Protection