Bridging Discrete and Continuous Logicin Automated Reasoning Systems
Christoph Kohlhepp · International Journal of Data Science and Big Data Analytics · 2023
In this paper we will explore the connection between Functional Programming and reasoning.Functional Programmingis often advanced as a means to increase type safety, write correct programs, or simply to pursue brevity and succinctness in program design.Much less emphasized, but just as powerful, is the connection between functional programming and logic-between functional programming and automated reasoning.On our journey we will consider object orientation, relational databases, and a Lisp based system called Powerloom, a Knowledge Representation and Reasoning System that can represent both (A) discrete mathematics as well as; (B) quantitative models such as regression as used instatistics.Powerloom is being developed at the Intelligent Systems Division at the University of Southern Californiaand was funded by Defence Advanced Projects Agency (DARPA).Along the way, we will look at a system called Coq,a theorem prover for OCaml.This is part 2 of a 3 part series.Part 1 is the Anatomy of a Puzzle.