title:
Typed Decidable First-Order Logics for Reasoning about Unbounded Resources

Abstract :
 We investigated the possibility of developing a decidable logic which allows
 expressing many of the real word specifications.
 The idea is to define a decidable subset of many sorted first order logic.
 The problem of classifying fragments of first-order logic with respect to the
 decidability and complexity of the satisfiability problem has long been a
 major topic in the study of classical logic.
 In the book of Egon Bn decidable fragment. For example consider the formula:
 Forall x,y:A exists z:B | G(x,y,z)
 where G is quantifier free formula with identity. This formula is unsolvable
 according the classical results although it is obvious that this class has
 the finite model property. So we can see that adding types simplifies the
 complexity of mixed quantifiers if they quantify different types.
 We noticed that in many real word verification problems the quantification is
 on different types in such way that the relations between types remain simple.
 Our main result is developing of decidable fragment to many sorted first
 order logic with limited use of functions and transitive closer that captures
 many of real word specifications.