OpenQED is a nascent personal project in automated theorem proving (ATP) for first order logic. The purpose has been educational -- to learn about ATP in general, with a particular interest in its application to problems in software construction and verification.

Results so far include a Java class library for parsing, structuring, and basic manipulation of problems in first order logic. The design of this library is heavily influenced by the TPTP problem library, which is used as a primary source for testing.

The purpose of this site is to share results as they're developed. Source code will be posted as it matures and gains features worth sharing.

Thanks for stopping by!

Guy Shefner
email: my first name @ my last name .com

Overview of NamedId classes

Overview of FormulaNode classes

Overview of Sentence classes