Automated reasoning in some local extensions of ordered structures
We give a uniform method for automated reasoning in several types of extensions of ordered algebraic structures (definitional extensions, extensions with boundedness axioms or with monotonicity axioms). We show that such extensions are local and, hence, efficient methods for hierarchical reasoning exist in all these cases.
automated reasoning hierarchical reasoning lattice-ordered structures monotone functions mv-algebras godel algebras