AI Planning Languages Semantics
From MaRDI portal
- 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 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: AI Planning Languages Semantics
