52 lines
No EOL
4.3 KiB
HTML
52 lines
No EOL
4.3 KiB
HTML
<!DOCTYPE html>
|
|
<html>
|
|
<head>
|
|
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
|
|
<title>CLiki: Prolog Technology Theorem Prover</title>
|
|
<link rel="alternate" type="application/atom+xml" title="ATOM feed of edits to current article"
|
|
href="https://www.cliki.net/site/feed/article.atom?title=Prolog%20Technology%20Theorem%20Prover">
|
|
<link rel="stylesheet" href="static/css/style.css">
|
|
<link rel="stylesheet" href="static/css/colorize.css">
|
|
</head>
|
|
|
|
<body>
|
|
<span class="hidden">CLiki - Prolog Technology Theorem Prover</span>
|
|
<div id="content"><div id="content-area"><div id="article-title">Prolog Technology Theorem Prover</div><div id="article">The Prolog Technology Theorem Prover (<a href="http://www.ai.sri.com/~stickel/pttp-1i.lisp">PTTP</a>) is an implementation (in <a href="Common Lisp.html" class="internal">Common Lisp</a>) of the model elimination theorem-proving procedure that extends <a href="Prolog.html" class="category">Prolog</a> to the full first-order predicate calculus. PTTP differs from Prolog in its use of: (1) <a href="unification.html" class="category">unification</a> with the occurs check for soundness, (2) depth-first iterative deepening search instead of unbounded depth-first search to make the search strategy complete, and (3) the model elimination inference rule that is added to Prolog inferences to make the inference system complete. PTTP also extends Prolog by providing the capability of printing the proofs it finds. Because PTTP compiles the clauses of a problem, its inference rate is very high. Because PTTP uses depth-first search, its storage requirements are low and term size need not be limited to reduce memory usage at the expense of completeness. PTTP's simple architecture facilitates its adaptation and use in applications.<p>It is available <a href="http://www.ai.sri.com/~stickel/pttp.html">here</a> under a <a href="BSD.html" class="category">BSD</a>-like license.<p><hr>
|
|
<a href="Application.html" class="category">Application</a> <a href="Theorem Provers.html" class="category">Theorem Provers</a></div></div>
|
|
<div id="footer" class="buttonbar"><ul><li><a href="Prolog Technology Theorem Prover.html">Current version</a></li>
|
|
<li><a href="https://www.cliki.net/site/history?article=Prolog%20Technology%20Theorem%20Prover">History</a></li>
|
|
<li><a href="https://www.cliki.net/site/backlinks?article=Prolog%20Technology%20Theorem%20Prover">Backlinks</a></li><li><a href="https://www.cliki.net/site/edit-article?title=Prolog%20Technology%20Theorem%20Prover&from-revision=3809022186">Edit</a></li><li><a href="https://www.cliki.net/site/edit-article?create=t">Create</a></li></ul></div>
|
|
</div>
|
|
<div id="header-buttons" class="buttonbar">
|
|
<ul>
|
|
<li><a href="https://www.cliki.net/">Home</a></li>
|
|
<li><a href="https://www.cliki.net/site/recent-changes">Recent Changes</a></li>
|
|
<li><a href="CLiki.html">About</a></li>
|
|
<li><a href="Text Formatting.html">Text Formatting</a></li>
|
|
<li><a href="https://www.cliki.net/site/tools">Tools</a></li>
|
|
</ul>
|
|
<div id="search">
|
|
<form action="https://www.cliki.net/site/search">
|
|
<label for="search_query" class="hidden">Search CLiki</label>
|
|
<input type="text" name="query" id="search_query" value="" />
|
|
<input type="submit" value="search" />
|
|
</form>
|
|
</div>
|
|
</div>
|
|
<div id="pageheader">
|
|
<div id="header">
|
|
<span id="logo">CLiki</span>
|
|
<span id="slogan">the common lisp wiki</span>
|
|
<div id="login"><form method="post" action="https://www.cliki.net/site/login">
|
|
<label for="login_name" class="hidden">Account name</label>
|
|
<input type="text" name="name" id="login_name" class="login_input" />
|
|
<label for= "login_password" class="hidden">Password</label>
|
|
<input type="password" name="password" id="login_password" class="login_input" />
|
|
<input type="submit" name="login" value="login" id="login_submit" /><br />
|
|
<div id="register"><a href="https://www.cliki.net/site/register">register</a></div>
|
|
<input type="submit" name="reset-pw" value="reset password" id="reset_pw" />
|
|
</form>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
</body></html> |