Actions for Representations of the language recognition problem for a theorem prover

Email RIS file
Bookmark
Report an Issue

Representations of the language recognition problem for a theorem prover

Author
Minker, J.
Published
Sep 1, 1972.
Physical Description
1 electronic document
Additional Creators
Vanderbrug, G. J.
Online Version

Availability

I Want It
I Want It

Finding items...

Restrictions on Access
Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access
Summary
Two representations of the language recognition problem for a theorem prover in first order logic are presented and contrasted. One of the representations is based on the familiar method of generating sentential forms of the language, and the other is based on the Cocke parsing algorithm. An augmented theorem prover is described which permits recognition of recursive languages. The state-transformation method developed by Cordell Green to construct problem solutions in resolution-based systems can be used to obtain the parse tree. In particular, the end-order traversal of the parse tree is derived in one of the representations. An inference system, termed the cycle inference system, is defined which makes it possible for the theorem prover to model the method on which the representation is based. The general applicability of the cycle inference system to state space problems is discussed. Given an unsatisfiable set S, where each clause has at most one positive literal, it is shown that there exists an input proof. The clauses for the two representations satisfy these conditions, as do many state space problems.
Other Subject(s)
Collection
NASA Technical Reports Server (NTRS) Collection.
Note
Document ID: 19730011905.
Accession ID: 73N20632.
TR-199.
NASA-CR-131402.
Terms of Use and Reproduction
No Copyright.
View MARC record | catkey: 15749837