Commit bdb0dfd1 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

Verified_SAT_Based_AI_Planning website [NB corrected some \cite commands and...

Verified_SAT_Based_AI_Planning website [NB corrected some \cite commands and deleted some excess files]
parent 0113b6493114
......@@ -7550,6 +7550,22 @@ abstract =
either language as well the correctness of potential solutions. The
formalisation in this entry was described in an earlier publication.
 
[Verified_SAT_Based_AI_Planning]
title = Verified SAT-Based AI Planning
author = Mohammad Abdulaziz <http://home.in.tum.de/~mansour/>, Friedrich Kurz
topic = Computer science/Artificial intelligence
date = 2020-10-29
notify = mohammad.abdulaziz8@gmail.com
abstract =
We present an executable formally verified SAT encoding of classical
AI planning that is based on the encodings by Kautz and Selman and the
one by Rintanen et al. The encoding was experimentally tested and
shown to be usable for reasonably sized standard AI planning
benchmarks. We also use it as a reference to test a state-of-the-art
SAT-based planner, showing that it sometimes falsely claims that
problems have no solutions of certain lengths. The formalisation in
this submission was described in an independent publication.
[Gromov_Hyperbolicity]
title = Gromov Hyperbolicity
author = Sebastien Gouezel<>
......
......@@ -146,7 +146,9 @@ formalisation in this entry was described in an earlier publication.</td>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Certification_Monads.html">Certification_Monads</a>, <a href="Containers.html">Containers</a>, <a href="Propositional_Proof_Systems.html">Propositional_Proof_Systems</a>, <a href="Show.html">Show</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Verified_SAT_Based_AI_Planning.html">Verified_SAT_Based_AI_Planning</a> </td></tr>
</tbody>
......
......@@ -132,7 +132,7 @@ MathJax = {
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Affine_Arithmetic.html">Affine_Arithmetic</a>, <a href="Comparison_Sort_Lower_Bound.html">Comparison_Sort_Lower_Bound</a>, <a href="Formula_Derivatives.html">Formula_Derivatives</a>, <a href="Higher_Order_Terms.html">Higher_Order_Terms</a>, <a href="Jinja.html">Jinja</a>, <a href="List_Update.html">List_Update</a>, <a href="LTL_to_DRA.html">LTL_to_DRA</a>, <a href="MSO_Regex_Equivalence.html">MSO_Regex_Equivalence</a>, <a href="Nested_Multisets_Ordinals.html">Nested_Multisets_Ordinals</a>, <a href="Ordinary_Differential_Equations.html">Ordinary_Differential_Equations</a>, <a href="Planarity_Certificates.html">Planarity_Certificates</a>, <a href="Quick_Sort_Cost.html">Quick_Sort_Cost</a>, <a href="Randomised_Social_Choice.html">Randomised_Social_Choice</a>, <a href="Refine_Imperative_HOL.html">Refine_Imperative_HOL</a>, <a href="Smith_Normal_Form.html">Smith_Normal_Form</a> </td></tr>
<td class="data"><a href="Affine_Arithmetic.html">Affine_Arithmetic</a>, <a href="Comparison_Sort_Lower_Bound.html">Comparison_Sort_Lower_Bound</a>, <a href="Formula_Derivatives.html">Formula_Derivatives</a>, <a href="Higher_Order_Terms.html">Higher_Order_Terms</a>, <a href="Jinja.html">Jinja</a>, <a href="List_Update.html">List_Update</a>, <a href="LTL_to_DRA.html">LTL_to_DRA</a>, <a href="MSO_Regex_Equivalence.html">MSO_Regex_Equivalence</a>, <a href="Nested_Multisets_Ordinals.html">Nested_Multisets_Ordinals</a>, <a href="Ordinary_Differential_Equations.html">Ordinary_Differential_Equations</a>, <a href="Planarity_Certificates.html">Planarity_Certificates</a>, <a href="Quick_Sort_Cost.html">Quick_Sort_Cost</a>, <a href="Randomised_Social_Choice.html">Randomised_Social_Choice</a>, <a href="Refine_Imperative_HOL.html">Refine_Imperative_HOL</a>, <a href="Smith_Normal_Form.html">Smith_Normal_Form</a>, <a href="Verified_SAT_Based_AI_Planning.html">Verified_SAT_Based_AI_Planning</a> </td></tr>
......
......@@ -141,7 +141,7 @@ model existence.</td>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a> </td></tr>
<td class="data"><a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a>, <a href="Verified_SAT_Based_AI_Planning.html">Verified_SAT_Based_AI_Planning</a> </td></tr>
......
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>Verified SAT-Based AI Planning - Archive of Formal Proofs
</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<link rel="alternate" type="application/rss+xml" title="RSS" href="../rss.xml">
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax = {
tex: {
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
processEscapes: true,
svg: {
fontCache: 'global'
}
};
</script>
<script id="MathJax-script" async src="../components/mathjax/es5/tex-mml-chtml.js"></script>
</head>
<body class="mathjax_ignore">
<table width="100%">
<tbody>
<tr>
<!-- Navigation -->
<td width="20%" align="center" valign="top">
<p>&nbsp;</p>
<a href="https://www.isa-afp.org/">
<img src="../images/isabelle.png" width="100" height="88" border=0>
</a>
<p>&nbsp;</p>
<p>&nbsp;</p>
<table class="nav" width="80%">
<tr>
<td class="nav" width="100%"><a href="../index.html">Home</a></td>
</tr>
<tr>
<td class="nav"><a href="../about.html">About</a></td>
</tr>
<tr>
<td class="nav"><a href="../submitting.html">Submission</a></td>
</tr>
<tr>
<td class="nav"><a href="../updating.html">Updating Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../using.html">Using Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../search.html">Search</a></td>
</tr>
<tr>
<td class="nav"><a href="../statistics.html">Statistics</a></td>
</tr>
<tr>
<td class="nav"><a href="../topics.html">Index</a></td>
</tr>
<tr>
<td class="nav"><a href="../download.html">Download</a></td>
</tr>
</table>
<p>&nbsp;</p>
<p>&nbsp;</p>
</td>
<!-- Content -->
<td width="80%" valign="top">
<div align="center">
<p>&nbsp;</p>
<h1> <font class="first">V</font>erified
<font class="first">S</font>AT-Based
<font class="first">A</font>I
<font class="first">P</font>lanning
</h1>
<p>&nbsp;</p>
<table width="80%" class="data">
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Verified SAT-Based AI Planning</td>
</tr>
<tr>
<td class="datahead">
Authors:
</td>
<td class="data">
<a href="http://home.in.tum.de/~mansour/">Mohammad Abdulaziz</a> and
Friedrich Kurz
</td>
</tr>
<tr>
<td class="datahead">Submission date:</td>
<td class="data">2020-10-29</td>
</tr>
<tr>
<td class="datahead" valign="top">Abstract:</td>
<td class="abstract mathjax_process">
We present an executable formally verified SAT encoding of classical
AI planning that is based on the encodings by Kautz and Selman and the
one by Rintanen et al. The encoding was experimentally tested and
shown to be usable for reasonably sized standard AI planning
benchmarks. We also use it as a reference to test a state-of-the-art
SAT-based planner, showing that it sometimes falsely claims that
problems have no solutions of certain lengths. The formalisation in
this submission was described in an independent publication.</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Verified_SAT_Based_AI_Planning-AFP,
author = {Mohammad Abdulaziz and Friedrich Kurz},
title = {Verified SAT-Based AI Planning},
journal = {Archive of Formal Proofs},
month = oct,
year = 2020,
note = {\url{http://isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td>
</tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a>, <a href="List-Index.html">List-Index</a>, <a href="Propositional_Proof_Systems.html">Propositional_Proof_Systems</a> </td></tr>
</tbody>
</table>
<p></p>
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Verified_SAT_Based_AI_Planning/outline.pdf">Proof outline</a><br>
<a href="../browser_info/current/AFP/Verified_SAT_Based_AI_Planning/document.pdf">Proof document</a>
</td>
</tr>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Verified_SAT_Based_AI_Planning/index.html">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="../release/afp-Verified_SAT_Based_AI_Planning-current.tar.gz">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
</body>
</html>
\ No newline at end of file
......@@ -88,6 +88,15 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<tr>
<td class="head">2020</td>
</tr>
<tr>
<td class="entry">
2020-10-29: <a href="entries/Verified_SAT_Based_AI_Planning.html">Verified SAT-Based AI Planning</a>
<br>
Authors:
<a href="http://home.in.tum.de/~mansour/">Mohammad Abdulaziz</a>
and Friedrich Kurz
</td>
</tr>
<tr>
<td class="entry">
2020-10-29: <a href="entries/AI_Planning_Languages_Semantics.html">AI Planning Languages Semantics</a>
......
......@@ -10,6 +10,22 @@
in the theorem prover Isabelle.
</description>
<pubDate>29 Oct 2020 00:00:00 +0000</pubDate>
<item>
<title>Verified SAT-Based AI Planning</title>
<link>https://www.isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html</link>
<guid>https://www.isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html</guid>
<dc:creator> Mohammad Abdulaziz, Friedrich Kurz </dc:creator>
<pubDate>29 Oct 2020 00:00:00 +0000</pubDate>
<description>
We present an executable formally verified SAT encoding of classical
AI planning that is based on the encodings by Kautz and Selman and the
one by Rintanen et al. The encoding was experimentally tested and
shown to be usable for reasonably sized standard AI planning
benchmarks. We also use it as a reference to test a state-of-the-art
SAT-based planner, showing that it sometimes falsely claims that
problems have no solutions of certain lengths. The formalisation in
this submission was described in an independent publication.</description>
</item>
<item>
<title>AI Planning Languages Semantics</title>
<link>https://www.isa-afp.org/entries/AI_Planning_Languages_Semantics.html</link>
......@@ -600,27 +616,5 @@ and the MacLaurin series of
&lt;em&gt;W&lt;/em&gt;&lt;sub&gt;0&lt;/sub&gt;(&lt;em&gt;x&lt;/em&gt;)
at &lt;em&gt;x&lt;/em&gt; = 0.&lt;/p&gt;</description>
</item>
<item>
<title>Gaussian Integers</title>
<link>https://www.isa-afp.org/entries/Gaussian_Integers.html</link>
<guid>https://www.isa-afp.org/entries/Gaussian_Integers.html</guid>
<dc:creator> Manuel Eberl </dc:creator>
<pubDate>24 Apr 2020 00:00:00 +0000</pubDate>
<description>
&lt;p&gt;The Gaussian integers are the subring &amp;#8484;[i] of the
complex numbers, i. e. the ring of all complex numbers with integral
real and imaginary part. This article provides a definition of this
ring as well as proofs of various basic properties, such as that they
form a Euclidean ring and a full classification of their primes. An
executable (albeit not very efficient) factorisation algorithm is also
provided.&lt;/p&gt; &lt;p&gt;Lastly, this Gaussian integer
formalisation is used in two short applications:&lt;/p&gt; &lt;ol&gt;
&lt;li&gt; The characterisation of all positive integers that can be
written as sums of two squares&lt;/li&gt; &lt;li&gt; Euclid&#39;s
formula for primitive Pythagorean triples&lt;/li&gt; &lt;/ol&gt;
&lt;p&gt;While elementary proofs for both of these are already
available in the AFP, the theory of Gaussian integers provides more
concise proofs and a more high-level view.&lt;/p&gt;</description>
</item>
</channel>
</rss>
This diff is collapsed.
......@@ -74,6 +74,7 @@
<h3>Artificial intelligence</h3>
<div class="list">
<a href="entries/AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a> &nbsp;
<a href="entries/Verified_SAT_Based_AI_Planning.html">Verified_SAT_Based_AI_Planning</a> &nbsp;
</div>
<h3>Automata and formal languages</h3>
<div class="list">
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment