Email Gateway (Jun 28 2026 at 16:37): Email Gateway (Jun 28 2026 at 16:37):From: Lawrence Paulson <lp15@cam.ac.uk>
Subject: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
I'm happy to announce yet another contribution, this time AI-powered and relating to AI. But this this STRIPS related to the original STRIPS?
Larry
Formalization of Lower-Bound Certificates for Optimal Classical Planning
Dmitriy Traytel
We formalize the framework of pseudo-Boolean lower-bound certificates for classical planning introduced by Dold, Helmert, Nordström, Röger and Schindler. A lower-bound certificate for a STRIPS (Simplified Theory of International Planning Representation and Scheduling) planning task and a bound B is a pseudo-Boolean circuit together with three proofs in the cutting planes proof system with reification; its validity guarantees that every plan of the task costs at least B, and hence that a plan of cost B is optimal. We prove the soundness of the certificate format (Theorem 1 of the paper) and formalize the paper's case study: certificates extracted from a run of the A* algorithm, with heuristic certificates for pattern database heuristics and for the maximum heuristic hmax, including the appendix material on efficiently proof-logging pattern databases. The main results state that a suitable snapshot of a terminated A* run yields a valid certificate and therefore proves the optimality of the plan it found. All locales are shown consistent by concrete interpretations, which also compose the pattern database certificate with the A* certificate, as intended by the paper.
https://isa-afp.org/entries/Lower_Bound_Certificates_Planning.html
Email Gateway (Jun 29 2026 at 19:16):From: waldinge <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
I think the original STRIPS acronym had a different meaning. Something like STanford Research Institute Planning System.
On Jun 28, 2026, at 9:36 AM, Lawrence Paulson <lp15@cam.ac.uk> wrote:
I'm happy to announce yet another contribution, this time AI-powered and relating to AI. But this this STRIPS related to the original STRIPS?
Larry
Formalization of Lower-Bound Certificates for Optimal Classical Planning
Dmitriy TraytelWe formalize the framework of pseudo-Boolean lower-bound certificates for classical planning introduced by Dold, Helmert, Nordström, Röger and Schindler. A lower-bound certificate for a STRIPS (Simplified Theory of International Planning Representation and Scheduling) planning task and a bound B is a pseudo-Boolean circuit together with three proofs in the cutting planes proof system with reification; its validity guarantees that every plan of the task costs at least B, and hence that a plan of cost B is optimal. We prove the soundness of the certificate format (Theorem 1 of the paper) and formalize the paper's case study: certificates extracted from a run of the A* algorithm, with heuristic certificates for pattern database heuristics and for the maximum heuristic hmax, including the appendix material on efficiently proof-logging pattern databases. The main results state that a suitable snapshot of a terminated A* run yields a valid certificate and therefore proves the optimality of the plan it found. All locales are shown consistent by concrete interpretations, which also compose the pattern database certificate with the A* certificate, as intended by the paper.
https://isa-afp.org/entries/Lower_Bound_Certificates_Planning.html
Email Gateway (Jun 29 2026 at 19:55):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
Now, this is EMBARRASSING for me. And I guess the perfect demonstration of how much one can trust these funny machines. This is the original STRIPS planning task format according to Dold et al. Their paper does not expand the acronym, so I didn’t notice/suspect that something is wrong in the abstract (I’m not sure which agent helped me draft that). Of course it is my responsibility to check the informal text as well. I will correct it.
Thanks and best wishes,
Dmitriy
On 29 Jun 2026, at 21.15, waldinge <cl-isabelle-users@lists.cam.ac.uk> wrote:
I think the original STRIPS acronym had a different meaning. Something like STanford Research Institute Planning System.
On Jun 28, 2026, at 9:36 AM, Lawrence Paulson <lp15@cam.ac.uk<mailto:lp15@cam.ac.uk>> wrote:
I'm happy to announce yet another contribution, this time AI-powered and relating to AI. But this this STRIPS related to the original STRIPS?
Larry
Formalization of Lower-Bound Certificates for Optimal Classical Planning
Dmitriy Traytel
We formalize the framework of pseudo-Boolean lower-bound certificates for classical planning introduced by Dold, Helmert, Nordström, Röger and Schindler. A lower-bound certificate for a STRIPS (Simplified Theory of International Planning Representation and Scheduling) planning task and a bound B is a pseudo-Boolean circuit together with three proofs in the cutting planes proof system with reification; its validity guarantees that every plan of the task costs at least B, and hence that a plan of cost B is optimal. We prove the soundness of the certificate format (Theorem 1 of the paper) and formalize the paper's case study: certificates extracted from a run of the A* algorithm, with heuristic certificates for pattern database heuristics and for the maximum heuristic hmax, including the appendix material on efficiently proof-logging pattern databases. The main results state that a suitable snapshot of a terminated A* run yields a valid certificate and therefore proves the optimality of the plan it found. All locales are shown consistent by concrete interpretations, which also compose the pattern database certificate with the A* certificate, as intended by the paper.
https://isa-afp.org/entries/Lower_Bound_Certificates_Planning.html
Email Gateway (Jun 29 2026 at 20:03):From: waldinge <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
I didn't check, myself.---rw
On Jun 29, 2026, at 12:55 PM, Dmitriy Traytel (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:
Now, this is EMBARRASSING for me. And I guess the perfect demonstration of how much one can trust these funny machines. This is the original STRIPS planning task format according to Dold et al. Their paper does not expand the acronym, so I didn’t notice/suspect that something is wrong in the abstract (I’m not sure which agent helped me draft that). Of course it is my responsibility to check the informal text as well. I will correct it.
Thanks and best wishes,
DmitriyOn 29 Jun 2026, at 21.15, waldinge <cl-isabelle-users@lists.cam.ac.uk> wrote:
I think the original STRIPS acronym had a different meaning. Something like STanford Research Institute Planning System.
On Jun 28, 2026, at 9:36 AM, Lawrence Paulson <lp15@cam.ac.uk <mailto:lp15@cam.ac.uk>> wrote:
I'm happy to announce yet another contribution, this time AI-powered and relating to AI. But this this STRIPS related to the original STRIPS?
Larry
Formalization of Lower-Bound Certificates for Optimal Classical Planning
Dmitriy TraytelWe formalize the framework of pseudo-Boolean lower-bound certificates for classical planning introduced by Dold, Helmert, Nordström, Röger and Schindler. A lower-bound certificate for a STRIPS (Simplified Theory of International Planning Representation and Scheduling) planning task and a bound B is a pseudo-Boolean circuit together with three proofs in the cutting planes proof system with reification; its validity guarantees that every plan of the task costs at least B, and hence that a plan of cost B is optimal. We prove the soundness of the certificate format (Theorem 1 of the paper) and formalize the paper's case study: certificates extracted from a run of the A* algorithm, with heuristic certificates for pattern database heuristics and for the maximum heuristic hmax, including the appendix material on efficiently proof-logging pattern databases. The main results state that a suitable snapshot of a terminated A* run yields a valid certificate and therefore proves the optimality of the plan it found. All locales are shown consistent by concrete interpretations, which also compose the pattern database certificate with the A* certificate, as intended by the paper.
https://isa-afp.org/entries/Lower_Bound_Certificates_Planning.html <https://isa-afp.org/entries/Lower_Bound_Certificates_Planning.html>
Email Gateway (Jun 30 2026 at 02:55):From: Mohammad Abdulaziz <mohammad.abdulaziz8@gmail.com>
Subject: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
I think no one ever expands the acronym since STRIPS as used in modern
planning literature is a more abstract and also different format from the
original Stanford format. Eg the modern acronym refers to a format with only
ground atoms, while the original had more than just that.
Best,
Mohammad
On 29. Jun 2026, at 22:04, waldinge <cl-isabelle-users@lists.cam.ac.uk>
wrote:
I didn't check, myself.---rw
On Jun 29, 2026, at 12:55 PM, Dmitriy Traytel (via cl-isabelle-users
Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:
>
>
>
Now, this is EMBARRASSING for me. And I guess the perfect demonstration of
how much one can trust these funny machines. This is the original STRIPS
planning task format according to Dold et al. Their paper does not expand the
acronym, so I didn’t notice/suspect that something is wrong in the abstract
(I’m not sure which agent helped me draft that). Of course it is my
responsibility to check the informal text as well. I will correct it.
>
>
>
Thanks and best wishes,
>
Dmitriy
>
>
>
On 29 Jun 2026, at 21.15, waldinge <cl-isabelle-users@lists.cam.ac.uk>
wrote:
>
>
>
I think the original STRIPS acronym had a different meaning. Something
like STanford Research Institute Planning System.>
On Jun 28, 2026, at 9:36 AM, Lawrence Paulson
<lp15@cam.ac.uk> wrote:I'm happy to announce yet another contribution, this time AI-powered and
relating to AI. But this this STRIPS related to the original STRIPS?Larry
Formalization of Lower-Bound Certificates for Optimal Classical Planning
Dmitriy TraytelWe formalize the framework of pseudo-Boolean lower-bound certificates for
classical planning introduced by Dold, Helmert, Nordström, Röger and
Schindler. A lower-bound certificate for a STRIPS (Simplified Theory of
International Planning Representation and Scheduling) planning task and a
bound B is a pseudo-Boolean circuit together with three proofs in the
cutting planes proof system with reification; its validity guarantees that
every plan of the task costs at least B, and hence that a plan of cost B is
optimal. We prove the soundness of the certificate format (Theorem 1 of the
paper) and formalize the paper's case study: certificates extracted from a
run of the A* algorithm, with heuristic certificates for pattern database
heuristics and for the maximum heuristic hmax, including the appendix
material on efficiently proof-logging pattern databases. The main results
state that a suitable snapshot of a terminated A* run yields a valid
certificate and therefore proves the optimality of the plan it found. All
locales are shown consistent by concrete interpretations, which also compose
the pattern database certificate with the A* certificate, as intended by the
paper.
>
Email Gateway (Jun 30 2026 at 05:47):From: Prof Richard Fikes <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
The original STRIPS acronym was STanford Research Institute Problem Solver. (Thus spake the author.) (Also, see https://en.wikipedia.org/wiki/Stanford_Research_Institute_Problem_Solver.)
-Richard
On Jun 29, 2026, at 12:15 PM, waldinge <waldinger@ai.sri.com> wrote:
I think the original STRIPS acronym had a different meaning. Something like STanford Research Institute Planning System.
Email Gateway (Jun 30 2026 at 06:13):From: Mohammad Abdulaziz <mohammad.abdulaziz8@gmail.com>
Subject: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
That is correct, author.
I was commenting on why the LLM might have gotten it wrong: no one ever spells it out, at least in my experience (reviewing ca. 120 IJCAI/AAAI papers over the last 10 years).
Sent from my iPhone
On 30. Jun 2026, at 07:47, Prof Richard Fikes <cl-isabelle-users@lists.cam.ac.uk> wrote:
The original STRIPS acronym was STanford Research Institute Problem Solver. (Thus spake the author.) (Also, see https://en.wikipedia.org/wiki/Stanford_Research_Institute_Problem_Solver.)
-Richard
On Jun 29, 2026, at 12:15 PM, waldinge <waldinger@ai.sri.com> wrote:
I think the original STRIPS acronym had a different meaning. Something like STanford Research Institute Planning System.
Email Gateway (Jun 30 2026 at 09:51):From: Asta Halkjær Boserup <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
I hate it when my loaded dice do not roll as I expect them to! The loading must be imperfect.
I do enjoy that we went from the very local “Stanford Research Institute” in the actual acronym to the very grand “International” in the generated expansion.
It does sound very hype.
Asta
From: <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Mohammad Abdulaziz <mohammad.abdulaziz8@gmail.com>
Date: Tuesday, 30 June 2026 at 08.13
To: "fikes@stanford.edu" <fikes@stanford.edu>
Cc: Richard Waldinger <waldinger@ai.sri.com>, Lawrence Paulson <lp15@cam.ac.uk>, Kestrel Announcements <kestrel-announcements@kestrel.edu>, isabelle-users <isabelle-users@cl.cam.ac.uk>
Subject: Re: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
Du får ikke ofte mails fra mohammad.abdulaziz8@gmail.com. Få mere at vide om, hvorfor dette er vigtigt<https://aka.ms/LearnAboutSenderIdentification>
That is correct, author.
I was commenting on why the LLM might have gotten it wrong: no one ever spells it out, at least in my experience (reviewing ca. 120 IJCAI/AAAI papers over the last 10 years).
Sent from my iPhone
On 30. Jun 2026, at 07:47, Prof Richard Fikes <cl-isabelle-users@lists.cam.ac.uk> wrote:
The original STRIPS acronym was STanford Research Institute Problem Solver. (Thus spake the author.) (Also, see https://en.wikipedia.org/wiki/Stanford_Research_Institute_Problem_Solver<https://en.wikipedia.org/wiki/Stanford_Research_Institute_Problem_Solver>.)
-Richard
On Jun 29, 2026, at 12:15 PM, waldinge <waldinger@ai.sri.com> wrote:
I think the original STRIPS acronym had a different meaning. Something like STanford Research Institute Planning System.
Email Gateway (Jun 30 2026 at 20:05):From: waldinge <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical Planning
Now it is just "SRI". No "international"
On Jun 30, 2026, at 2:50 AM, Asta Halkjær Boserup (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:
I hate it when my loaded dice do not roll as I expect them to! The loading must be imperfect.
I do enjoy that we went from the very local “Stanford Research Institute” in the actual acronym to the very grand “International” in the generated expansion.
It does sound very hype.Asta
From: <cl-isabelle-users-request@lists.cam.ac.uk <mailto:cl-isabelle-users-request@lists.cam.ac.uk>> on behalf of Mohammad Abdulaziz <mohammad.abdulaziz8@gmail.com <mailto:mohammad.abdulaziz8@gmail.com>>
Date: Tuesday, 30 June 2026 at 08.13
To: "fikes@stanford.edu <mailto:fikes@stanford.edu>" <fikes@stanford.edu <mailto:fikes@stanford.edu>>
Cc: Richard Waldinger <waldinger@ai.sri.com <mailto:waldinger@ai.sri.com>>, Lawrence Paulson <lp15@cam.ac.uk <mailto:lp15@cam.ac.uk>>, Kestrel Announcements <kestrel-announcements@kestrel.edu <mailto:kestrel-announcements@kestrel.edu>>, isabelle-users <isabelle-users@cl.cam.ac.uk <mailto:isabelle-users@cl.cam.ac.uk>>
Subject: Re: [isabelle] New in the AFP: Lower-Bound Certificates for Optimal Classical PlanningDu får ikke ofte mails fra mohammad.abdulaziz8@gmail.com <mailto:mohammad.abdulaziz8@gmail.com>. Få mere at vide om, hvorfor dette er vigtigt <https://aka.ms/LearnAboutSenderIdentification>
That is correct, author.I was commenting on why the LLM might have gotten it wrong: no one ever spells it out, at least in my experience (reviewing ca. 120 IJCAI/AAAI papers over the last 10 years).
Sent from my iPhone
On 30. Jun 2026, at 07:47, Prof Richard Fikes <cl-isabelle-users@lists.cam.ac.uk <mailto:cl-isabelle-users@lists.cam.ac.uk>> wrote:
The original STRIPS acronym was STanford Research Institute Problem Solver. (Thus spake the author.) (Also, see https://en.wikipedia.org/wiki/Stanford_Research_Institute_Problem_Solver.)
-Richard
On Jun 29, 2026, at 12:15 PM, waldinge <waldinger@ai.sri.com <mailto:waldinger@ai.sri.com>> wrote:
I think the original STRIPS acronym had a different meaning. Something like STanford Research Institute Planning System.
Last updated: Jul 02 2026 at 07:34 UTC