LogicSolver

Team info

Team name: DeepSleep

Members: Chenyu Wang, Yifu Shen, Yuanyuan Zhao

Inspiration

Our teamates are all from mathematical background. We are trying to build something that can automatically check if a mathematical statement is true or not. It would be cool if there's something that can free you from tedious proof works.

What it does

Well, this project is actually not that powerful. It only checks whether a statement form is a tautology, which means "a statement always true". A user can interact with it through terminal. It accepts a statement form and outputs True for "is a tautology" and False for "not a tautology".

How we built it

We modeled the problem using OOP and implement the simplest bruteforce algorithm to find out whether a statement form is a tautology or not. We believe the problem itself is actually as hard as SAT, both are NP-hard.

Challenges we ran into

We spent half of the time on resolving the user input, including matching the parentheses, finding substructures and evaluate logic values, and spent the other half on implementing the algorithm.

Accomplishments that we're proud of

The program can "understand" a string input as a statement and produce output correctly given a proper input, well, for the most of the time.

What we learned

We read a few pages of a book about first order logic and learnt a few about how formal logic works.

What's next for LogicResolver

Our next goal is to implement logic axioms and algorithms to match statement with axioms. Once axiom system is functional, it would be possible to build set theory on it.

Built With

• python