Application of Simplification Theories.
Mauricio Osorio, Juan Carlos Nieves, Gabriel Cervantes · 2000
In this abstract we present different applications of "simplification of theories". By simplification of theories we understand a set of relations defined over a class of theories with a fixed language. The only two general properties that this relations respect are: First, that they are polynomial time computable. Second, if a theory P 1 is related to P under a transformation ( that is P 1 is obtained from P using a transformation ) and m is a model of P 1 , then m is also a model for P: We discuss applications in three different fields in applied logic: First order theory proving, Well behaved semantics and Answer set programming. In first order theory proving, given a consistent first order theory T and an atom a, we may be interested in the derivability of a by T , that is, T j= a? Using OTTER the problem is traduced as showing that T [ f:ag is inconsistent. Unfortunately, this may cause a loop in the process (using OTTER, a well known theorem proving system) when T [f:ag is cons...