A Relaxation Approach to Splitting in an Automatic Theorem Prover

Please use this identifier to cite or link to this item: http://dspace.mediu.edu.my:8181/xmlui/handle/1721.1/6217

Full metadata record

DC Field	Value	Language
dc.creator	Nevins, Arthur J.	-
dc.date	2004-10-04T14:46:21Z	-
dc.date	2004-10-04T14:46:21Z	-
dc.date	1974-01-01	-
dc.date.accessioned	2013-10-09T02:44:13Z	-
dc.date.available	2013-10-09T02:44:13Z	-
dc.date.issued	2013-10-09	-
dc.identifier	AIM-302	-
dc.identifier	http://hdl.handle.net/1721.1/6217	-
dc.identifier.uri	http://koha.mediu.edu.my:8181/xmlui/handle/1721	-
dc.description	The splitting of a problem into subproblems often involves the same variable appearing in more than one of the subproblems. This makes these subproblems dependent upon one another since a solution to one may not qualify as a solution to another. A two stage method of splitting is described which first obtains solutions by relaxing the dependency requirement and then attempts to reconcile solutions to different subproblems. The method has been realized as part of an automatic theorem prover programmed in LISP which takes advantage of the procedural power that LISP provides. The program has had success with sryptarithmetic problems, problems from blocks world, and has been used as asubroutine in a plane geometry theorem prover.	-
dc.format	9729642 bytes	-
dc.format	950478 bytes	-
dc.format	application/postscript	-
dc.format	application/pdf	-
dc.language	en_US	-
dc.relation	AIM-302	-
dc.title	A Relaxation Approach to Splitting in an Automatic Theorem Prover	-
Appears in Collections:	MIT Items

Files in This Item:

There are no files associated with this item.

DSpace JSPUI