Recasting Cohn's many sorted logic into a constrained logic
Department of Computer and Information Science
Master of Science
Sher, Richard B.
McHugh, James A.
Computer science --Mathematics.
Logic, Symbolic and mathematical.
The use of a many sorted logic for theorem proving carries many advantages over a traditional unsorted logic. By placing restrictions on the search space, a many sorted logic can significantly reduce the amount steps in the resolution process. However, as a logic becomes more efficient, it increases in complexity.
One of these efficient log ics is Cohn's Many Sorted Logic, LLAMA. It uses complex data structures such as the sort lattice and sort arrays to maintain information about the sorts. Recasting LLAMA into Bürckert's constrained logic will keep the functionality of LLAMA while using a format that reduces the complexity and maintains a more traditional resolution rule.
njit-etd1999-068 (54 pages ~ 1,957 KB pdf)
Please complete this Feedback Form to inform us about your experience using this website. It will assist us in better serving your information needs in the future. Thank You!
Created March 12, 2008