[isabelle] New in the AFP: More about God

Iâm happy to announce yet another proof of the existence of God. This article also has the objective of illustrating applications of proof assistants to logic in a broader sense.

As an aside, the same technique can be used to show that Satan does not exist. Sorry about that.

> Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
> Computers may help us to understand --not just verify-- philosophical arguments. By utilizing modern proof assistants in an iterative interpretive process, we can reconstruct and assess an argument by fully formal means. Through the mechanization of a variant of St. Anselm's ontological argument by E. J. Lowe, which is a paradigmatic example of a natural-language argument with strong ties to metaphysics and religion, we offer an ideal showcase for our computer-assisted interpretive method.


Larry Paulson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.