A state vector algebra for algorithmic implementation of second-order logic
This work addresses the challenge of automated theorem proving for logicians and computer scientists, but it appears incremental as it builds on existing mathematical frameworks without demonstrating broad practical applications.
The authors tackled the problem of automating theorem proving in first- and second-order logic by developing a state vector algebra framework that maps second-order logic relations onto an algorithmic system, enabling the recovery of all basic set theory theorems in an elementary way.
We present a mathematical framework for mapping second-order logic relations onto a simple state vector algebra. Using this algebra, basic theorems of set theory can be proven in an algorithmic way, hence by an expert system. We illustrate the use of the algebra with simple examples and show that, in principle, all theorems of basic set theory can be recovered in an elementary way. The developed technique can be used for an automated theorem proving in the 1st and 2nd order logic.