Verified SAT-Based AI Planning

MaRDI QIDQ7361650FDO

Authors Mohammad Abdulaziz, Friedrich Kurz

Publication date 29 October 2020

Cites work

• A Brief Overview of HOL4
• A constructive theory of regular languages in Coq
• A formalisation of finite automata using hereditarily finite sets
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• A formalization of powerlist algebra in ACL2
• A full formalization of SLD-resolution in the calculus of inductive constructions
• A note on succinct representations of graphs
• A note on the complexity of longest path problems related to graph coloring
• A note on two problems in connexion with graphs
• A verified SAT solver framework with learn, forget, restart, and incrementality
• A weighted CSP approach to cost-optimal planning
• Algorithms and Computation
• An approximation algorithm for the longest path problem in solid grid graphs
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• An Isabelle/HOL formalisation of Green's theorem
• Antichains and compositional algorithms for LTL synthesis
• Approximation and Fixed Parameter Subquadratic Algorithms for Radius and Diameter in Sparse Graphs
• AUTO2, a saturation-based heuristic prover for higher-order logic
• Automata, Languages and Programming
• Automatically generating abstractions for planning
• Better approximation algorithms for the graph diameter
• Color-coding
• Complexity Results for Nonmonotonic Logics
• Compositional reasoning in model checking
• Computing over-approximations with bounded model checking
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• Depth-First Search and Linear Graph Algorithms
• Diameter and maximum degree in Eulerian digraphs
• Efficient verified (UN)SAT certificate checking
• Fast approximation algorithms for the diameter and radius of sparse graphs
• Fast Estimation of Diameter and Shortest Paths (Without Matrix Multiplication)
• Fibonacci heaps and their uses in improved network optimization algorithms
• Finding a Longest Path in a Complete Multipartite Digraph
• Finding a Path of Superlogarithmic Length
• Formal proof - the four color theorem
• Formalization and implementation of modern SAT solvers
• Formalized proof systems for propositional logic
• Formalizing strong normalization proofs of explicit substitution calculi in ALF
• Formally verified algorithms for upper-bounding state space diameters
• Foundations of a functional approach to knowledge representation
• HOL with definitions: semantics, soundness, and a verified implementation
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Hypertree decompositions and tractable queries
• In defense of PDDL axioms
• Integer priority queues with decrease key in constant time and the single source shortest paths problem
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle. A generic theorem prover
• Light-weight containers for Isabelle: efficient, extensible, nestable
• Linear completeness thresholds for bounded model checking
• Maximum diameter of regular digraphs
• Merge-and-Shrink Abstraction
• More Algorithms for All-Pairs Shortest Paths in Weighted Graphs
• New Bounds on the Complexity of the Shortest Path Problem
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• On a routing problem
• On computing a longest path in a tree
• On the complexity of kings
• On the diameter of a graph
• On the exponent of all pairs shortest path problem
• On the magnitude of completeness thresholds in bounded model checking
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• Ordinal arithmetic: Algorithms and mechanization
• Planning as heuristic search
• Planning as satisfiability: heuristics
• Planning as satisfiability: parallel plans and algorithms for plan search
• Planning in a hierarchy of abstraction spaces
• Practical graph isomorphism. II.
• Radius, diameter, and minimum degree
• Rule extraction from decision trees with complex nominal data
• Simple regret optimization in online planning for Markov decision processes
• Some lambda calculus and type theory formalized
• State-variable planning under structural restrictions: algorithms and complexity
• STRIPS: A new approach to the application of theorem proving to problem solving
• Succinct representations of graphs
• Tableaux for verification of data-centric processes
• The calculus of constructions
• The complexity of propositional linear temporal logics
• The computational complexity of propositional STRIPS planning
• The diameter of almost Eulerian digraphs
• The diameter of directed graphs
• The fast downward planning system
• The influence of k-dependence on the complexity of planning
• The intuitive definition of Du Bois singularities
• The LAMA planner: guiding cost-based anytime planning with landmarks
• Theorem Proving in Higher Order Logics
• Theory and Applications of Satisfiability Testing
• Tractable plan existence does not imply tractable plan generation
• Verification, Model Checking, and Abstract Interpretation
• Verified over-approximation of the diameter of propositionally factored transition systems
• Verifying a Hotel Key Card System

This page was built for software: Verified SAT-Based AI Planning