User Portlet
| Discussions |
|---|
| The goal of my project was to implement a simple resolution based theorem prover for first order logic in the Wolfram Language. ##Conversion to Conjunctive Normal Form In order to be able to apply the resolution method to an arbitrary sentence... |