|
Abstract : |
Abstract: We have argued elsewhere that first order inference can be made more efficient by using non-standard syntax for first order logic. In this paper we define a syntax for first order logic based on the structure of natural language under Montague semantics. We show that, for a certain fairly expressive fragment of this language, satisfiability is polynomial time decidable. The polynomial time decision procedure can be used as a subroutine in general purpose inference systems and seems to be more powerful than analogous procedures based on either classical or taxonomic syntax. This paper appeared in Artificial Intelligence vol. 56, 1992. A postscript electronic source for this paper can be found in ftp.ai.mit.edu:/pub/dam/aij1.ps. A bibtex reference can be found in internet file ftp.ai.mit.edu:/pub/dam/dam.bib. 1, |
