> And yes to first order predicate calculus too! Just two weeks ago Chung-chieh Shan and I were explaining at NASSLLI the embedding in Haskell of the higher-order predicate logic with two base types (so-called Ty2). The embedding supports type-safe simplification of formulas (which was really needed for our applications). The embedding is extensible: you can add models and more constants.
http://okmij.org/ftp/gengo/NASSLLI10/course.html#semantics _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe