A more expressive formulation of many sorted logic
In ordinary first order logic, simple facts may acquire long representing formulas; partially responsible is the lack of sortal information about objects and predicates. Consequently, many sorted logic is a tool to achieve more compact representations of knowledge in AI and to reduce the search space in automated deduction. In this paper, the author introduces a many sorted logic, which he calls LLAMA (at least the name ``logic lacking a meaningful acronym should not be taken serious). The basic concepts are sorting domains and sorting functions. Sorts are represented by the Boolean lattice of the set of subsets of sort symbols. Sorting functions serve to assign sorts to function- and predicate symbols; several alternatives to define sorting functions for logical connectives (particularly for \(\vee)\) are presented. Formally, there is some similarity to 4-valued logic, because besides TRUE and FALSE we have the values ``either true or false and ``nonsense (however, these are sort values, not truth values). A key notion is the concept of sort array, which is a tool to assign sorts to formulas. By associating a sort array with a formula F, one gets the sort of F in a sortal environment \((= assignment\) of sorts to variables); an algorithm to determine the sort of formulas in a sortal environment is given. Semantics for LLAMA is defined formally and many sorted inference rules are introduced, among them many sorted resolution for clausal forms. Finally, the author gives a detailed comparison with other approaches, particularly with that off \textit{C. Walther} [A many sorted calculus based on resolution and paramodulation, Proc. IJCAI-83, Karlsruhe, William Kaufmann, 882-899 (1983; for a general review of these proceedings see Zbl 0536.68074)]. The example of ``Schubert's steamroller is used to demonstrate the strong power of LLAMA; the problem is represented by 3 clauses only (compared with 27 in ordinary first order logic and 12 in Walther's logic).
- The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
- An order-sorted logic for knowledge representation systems
- Exploiting lattices in a theory of space and time
- Completing sort hierarchies
- Unification in sort theories and its applications
- Many-sorted first-order composition-nominative logic as institution
- Tesseral spatio-temporal reasoning for multi-dimensional data
- A typed resolution principle for deduction with conditional typing theory
- Resolution for label-based formulas in hierarchical representation
- scientific article; zbMATH DE number 4053066 (Why is no real title available?)
- Reasoning without believing: on the mechanisation of presuppositions and partiality
- scientific article; zbMATH DE number 6139879 (Why is no real title available?)
- Moss' logic for ordered coalgebras
- A mechanization of strong Kleene logic for partial functions
- Carving up space: steps towards construction of an absolutely complete theory of spatial regions
- Tableau methods for a logic with term declarations
- Strict coherence of conditional rewriting modulo axioms
- Representation, verification, and visualization of Tarskian interpretations for typed first-order logic
- Order-sorted logic programming with predicate hierarchy
This page was built for publication: A more expressive formulation of many sorted logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1101261)
