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

Entry for AI_Planning_Languages_Semantics, including new topic "Computer...

Entry for AI_Planning_Languages_Semantics, including new topic "Computer science/Artificial intelligence" and URLs for the authors
parent 93f41fb311c0
......@@ -7519,7 +7519,7 @@ abstract =
 
[Green]
title = An Isabelle/HOL formalisation of Green's Theorem
author = Mohammad Abdulaziz <mailto:mohammad.abdulaziz8@gmail.com>, Lawrence C. Paulson <http://www.cl.cam.ac.uk/~lp15/>
author = Mohammad Abdulaziz <http://home.in.tum.de/~mansour/>, Lawrence C. Paulson <http://www.cl.cam.ac.uk/~lp15/>
topic = Mathematics/Analysis
date = 2018-01-11
notify = mohammad.abdulaziz8@gmail.com, lp15@cam.ac.uk
......@@ -7534,6 +7534,22 @@ abstract =
Instead we appeal to a homological argument about equivalences between
paths.
 
[AI_Planning_Languages_Semantics]
title = AI Planning Languages Semantics
author = Mohammad Abdulaziz <http://home.in.tum.de/~mansour/>, Peter Lammich <http://www21.in.tum.de/~lammich>
topic = Computer science/Artificial intelligence
date = 2020-10-29
notify = mohammad.abdulaziz8@gmail.com
abstract =
This is an Isabelle/HOL formalisation of the semantics of the
multi-valued planning tasks language that is used by the planning
system Fast-Downward, the STRIPS fragment of the Planning Domain
Definition Language (PDDL), and the STRIPS soundness meta-theory
developed by Vladimir Lifschitz. It also contains formally verified
checkers for checking the well-formedness of problems specified in
either language as well the correctness of potential solutions. The
formalisation in this entry was described in an earlier publication.
[Gromov_Hyperbolicity]
title = Gromov Hyperbolicity
author = Sebastien Gouezel<>
......@@ -9781,14 +9797,14 @@ abstract =
be merged and provide proofs of the various conditions which must hold
for these abstractions to subsume their ungeneralised counterparts. A
Code Generator setup to create executable Scala code is also defined.
[Physical_Quantities]
title = A Sound Type System for Physical Quantities, Units, and Measurements
author = Simon Foster <https://www-users.cs.york.ac.uk/~simonf/>, Burkhart Wolff <https://www.lri.fr/~wolff/>
topic = Mathematics/Physics, Computer science/Programming languages/Type systems
date = 2020-10-20
notify = simon.foster@york.ac.uk, wolff@lri.fr
abstract =
abstract =
The present Isabelle theory builds a formal model for both the
International System of Quantities (ISQ) and the International System
of Units (SI), which are both fundamental for physics and engineering.
......
Computer science
Artificial intelligence
Automata and formal languages
Algorithms
Graph
......
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>AI Planning Languages Semantics - 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">A</font>I
<font class="first">P</font>lanning
<font class="first">L</font>anguages
<font class="first">S</font>emantics
</h1>
<p>&nbsp;</p>
<table width="80%" class="data">
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">AI Planning Languages Semantics</td>
</tr>
<tr>
<td class="datahead">
Authors:
</td>
<td class="data">
<a href="http://home.in.tum.de/~mansour/">Mohammad Abdulaziz</a> and
Peter Lammich
</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">
This is an Isabelle/HOL formalisation of the semantics of the
multi-valued planning tasks language that is used by the planning
system Fast-Downward, the STRIPS fragment of the Planning Domain
Definition Language (PDDL), and the STRIPS soundness meta-theory
developed by Vladimir Lifschitz. It also contains formally verified
checkers for checking the well-formedness of problems specified in
either language as well the correctness of potential solutions. The
formalisation in this entry was described in an earlier publication.</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{AI_Planning_Languages_Semantics-AFP,
author = {Mohammad Abdulaziz and Peter Lammich},
title = {AI Planning Languages Semantics},
journal = {Archive of Formal Proofs},
month = oct,
year = 2020,
note = {\url{http://isa-afp.org/entries/AI_Planning_Languages_Semantics.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="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>
</tbody>
</table>
<p></p>
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/AI_Planning_Languages_Semantics/outline.pdf">Proof outline</a><br>
<a href="../browser_info/current/AFP/AI_Planning_Languages_Semantics/document.pdf">Proof document</a>
</td>
</tr>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/AI_Planning_Languages_Semantics/index.html">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="../release/afp-AI_Planning_Languages_Semantics-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
......@@ -135,7 +135,7 @@ MathJax = {
<td class="data"><a href="Partial_Function_MR.html">Partial_Function_MR</a>, <a href="Show.html">Show</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="WOOT_Strong_Eventual_Consistency.html">WOOT_Strong_Eventual_Consistency</a>, <a href="XML.html">XML</a> </td></tr>
<td class="data"><a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a>, <a href="WOOT_Strong_Eventual_Consistency.html">WOOT_Strong_Eventual_Consistency</a>, <a href="XML.html">XML</a> </td></tr>
......
......@@ -158,7 +158,7 @@ provide generators for canonical type class instantiations
<td class="data"><a href="Automatic_Refinement.html">Automatic_Refinement</a>, <a href="Collections.html">Collections</a>, <a href="Deriving.html">Deriving</a>, <a href="Finger-Trees.html">Finger-Trees</a>, <a href="Regular-Sets.html">Regular-Sets</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="MFODL_Monitor_Optimized.html">MFODL_Monitor_Optimized</a>, <a href="MFOTL_Monitor.html">MFOTL_Monitor</a> </td></tr>
<td class="data"><a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a>, <a href="MFODL_Monitor_Optimized.html">MFODL_Monitor_Optimized</a>, <a href="MFOTL_Monitor.html">MFOTL_Monitor</a> </td></tr>
......
......@@ -140,7 +140,9 @@ 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>
</tbody>
......
......@@ -152,7 +152,7 @@ datatypes similar to Haskell's "deriving Show".</td>
<td class="data"><a href="Deriving.html">Deriving</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Affine_Arithmetic.html">Affine_Arithmetic</a>, <a href="CakeML.html">CakeML</a>, <a href="CakeML_Codegen.html">CakeML_Codegen</a>, <a href="Certification_Monads.html">Certification_Monads</a>, <a href="Dict_Construction.html">Dict_Construction</a>, <a href="Monad_Memo_DP.html">Monad_Memo_DP</a>, <a href="Polynomial_Factorization.html">Polynomial_Factorization</a>, <a href="Polynomials.html">Polynomials</a>, <a href="Real_Impl.html">Real_Impl</a>, <a href="XML.html">XML</a> </td></tr>
<td class="data"><a href="Affine_Arithmetic.html">Affine_Arithmetic</a>, <a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a>, <a href="CakeML.html">CakeML</a>, <a href="CakeML_Codegen.html">CakeML_Codegen</a>, <a href="Certification_Monads.html">Certification_Monads</a>, <a href="Dict_Construction.html">Dict_Construction</a>, <a href="Monad_Memo_DP.html">Monad_Memo_DP</a>, <a href="Polynomial_Factorization.html">Polynomial_Factorization</a>, <a href="Polynomials.html">Polynomials</a>, <a href="Real_Impl.html">Real_Impl</a>, <a href="XML.html">XML</a> </td></tr>
......
......@@ -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/AI_Planning_Languages_Semantics.html">AI Planning Languages Semantics</a>
<br>
Authors:
<a href="http://home.in.tum.de/~mansour/">Mohammad Abdulaziz</a>
and Peter Lammich
</td>
</tr>
<tr>
<td class="entry">
2020-10-20: <a href="entries/Physical_Quantities.html">A Sound Type System for Physical Quantities, Units, and Measurements</a>
......
......@@ -9,7 +9,23 @@
and larger scientific developments, mechanically checked
in the theorem prover Isabelle.
</description>
<pubDate>20 Oct 2020 00:00:00 +0000</pubDate>
<pubDate>29 Oct 2020 00:00:00 +0000</pubDate>
<item>
<title>AI Planning Languages Semantics</title>
<link>https://www.isa-afp.org/entries/AI_Planning_Languages_Semantics.html</link>
<guid>https://www.isa-afp.org/entries/AI_Planning_Languages_Semantics.html</guid>
<dc:creator> Mohammad Abdulaziz, Peter Lammich </dc:creator>
<pubDate>29 Oct 2020 00:00:00 +0000</pubDate>
<description>
This is an Isabelle/HOL formalisation of the semantics of the
multi-valued planning tasks language that is used by the planning
system Fast-Downward, the STRIPS fragment of the Planning Domain
Definition Language (PDDL), and the STRIPS soundness meta-theory
developed by Vladimir Lifschitz. It also contains formally verified
checkers for checking the well-formedness of problems specified in
either language as well the correctness of potential solutions. The
formalisation in this entry was described in an earlier publication.</description>
</item>
<item>
<title>A Sound Type System for Physical Quantities, Units, and Measurements</title>
<link>https://www.isa-afp.org/entries/Physical_Quantities.html</link>
......@@ -606,21 +622,5 @@ formula for primitive Pythagorean triples&lt;/li&gt; &lt;/ol&gt;
available in the AFP, the theory of Gaussian integers provides more
concise proofs and a more high-level view.&lt;/p&gt;</description>
</item>
<item>
<title>Matrices for ODEs</title>
<link>https://www.isa-afp.org/entries/Matrices_for_ODEs.html</link>
<guid>https://www.isa-afp.org/entries/Matrices_for_ODEs.html</guid>
<dc:creator> Jonathan Julian Huerta y Munive </dc:creator>
<pubDate>19 Apr 2020 00:00:00 +0000</pubDate>
<description>
Our theories formalise various matrix properties that serve to
establish existence, uniqueness and characterisation of the solution
to affine systems of ordinary differential equations (ODEs). In
particular, we formalise the operator and maximum norm of matrices.
Then we use them to prove that square matrices form a Banach space,
and in this setting, we show an instance of Picard-Lindelöf’s
theorem for affine systems of ODEs. Finally, we use this formalisation
to verify three simple hybrid programs.</description>
</item>
</channel>
</rss>
This diff is collapsed.
......@@ -71,7 +71,11 @@
<h2>Computer science</h2>
<div class="list">
</div>
<h3>Automata and formal languages</h3>
<h3>Artificial intelligence</h3>
<div class="list">
<a href="entries/AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a> &nbsp;
</div>
<h3>Automata and formal languages</h3>
<div class="list">
<a href="entries/Partial_Order_Reduction.html">Partial_Order_Reduction</a> &nbsp;
<a href="entries/C2KA_DistributedSystems.html">C2KA_DistributedSystems</a> &nbsp;
......
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