`IMP- to SAT`on HOL level, functional correctness

wimmers / poly-reductions

Polynomial-time reductions in Isabelle/HOL

2 stars 13 forks source link

`IMP- to SAT`on HOL level, functional correctness #20

Open maxhaslbeck opened 3 years ago

maxhaslbeck commented 3 years ago

Problem: given a IMP- program c and input x and a number of steps t give a SAS+ planning problem that has a solution iff the program terminates with result 1
show each variable in the computation of c on x takes only at most t many values
implement PI :: IMP- => nat => state => SAS+
prove correctness of the construction

this includes #8

maxhaslbeck commented 3 years ago

@notiho provides a verified translation from IMP- to SAS+. @mabdula provides a verified translation from SAS+ to SAT. Theory IMP_Minus_To_SAT.thy collects the theorems that need to be plugged together.