An automated theorem prover for first-order predicate logic. Given a valid closed formula, it will find a proof using resolution principle if possible. Type a formula below or click here (multiple times) to see examples.
Created by Kazushi Kitaya. For source code and descriptions, refer to the GitHub repository.