Computational logic for biomedicine and neurosciences

A computational logic is a logic that enables proofs on the computer, that is, mechanized reasoning: one of the foundations of artificial intelligence. This chapter advocates the use of computational logic as a unified and safe approach to both specifying and analyzing biological systems. It presents two applications areas of the approach: biomedicine and neuroscience. The chapter presents the use of logical frameworks, and more precisely linear logic, to model and analyzes biological systems in the biomedicine area. It then focuses on metastatic breast cancer, which is representative of the approach. The chapter also uses Coq to prove four important properties of neurons and archetypes. It provides a discrete version of the leaky integrate and fire model. The chapter presents the Coq model for neural networks, which includes definitions of neurons, operations on them and the combination of neurons into archetypes.