Proof Assistants

 

Prolog

from ref :

Is Prolog a theorem prover? Richard O'Keefe said: "Prolog is an efficient programming language because it is a very stupid theorem prover".

Thus, there is a connection between Prolog and theorem proving. In fact, execution of a Prolog program can be regarded as a special case of resolution, called SLDNF resolution.

However, Prolog is not a full-fledged theorem prover. In particular, Prolog is logically incomplete due to its depth-first search strategy: Prolog may be unable to find a resolution refutation even if one exists.

 

 

 

 

 

 

 

 

 

 

 


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

cover Executable UML - Covers compiler issues but no code
cover Executable UML - concentrates on patterns

cover Fast Track UML 2.0 - useful for people who know some UML but are upgrading to 2.0

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to this site, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2021 Martin John Baker - All rights reserved - privacy policy.