Improving the expressiveness of many sorted logic

摘要: Many sorted logics can allow an increase in deductive efficiency by eliminating useless branches of the search space, but are usually formulated so that their expressive power is severely limited. The many logic described here unusual quantifiers unsorted; restriction on range a quantified variable derives from argument positions function and predicate symbols it occupies; associated with every non-logical symbol sorting which describes how its sort varies sorts inputs; polymorphic functions predicates thus easily expressible statements requiring several assertions may be compactly expressed single assertion. The structure arbitrary lattice. Increased expressiveness obtained allowing term to more general than position occupies. Furthermore, three boolean (representing 'true', 'false' 'either true or false'), sometimes possible detect formula contradictory tautologous without resort inference rules. Inference rules for resolution based system discussed; these proved both sound complete.