The New Jersey Institute of Technology's
Electronic Theses & Dissertations Project

Title:	Recasting Cohn's many sorted logic into a constrained logic
Author:	Koelbl, Christopher Brendan
View Online:	njit-etd1999-068 (vii, 44 pages ~ 1.9 MB pdf)
Department:	Department of Computer and Information Science
Degree:	Master of Science
Program:	Computer Science
Document Type:	Thesis
Advisory Committee:	Scherl, Richard B. (Committee chair) Featheringham, Thomas (Committee member) McHugh, James A. (Committee member)
Date:	1999-05
Keywords:	Computer science --Mathematics. Logic, Symbolic and mathematical. Artificial intelligence.
Availability:	Unrestricted
Abstract:	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.