Proof assistant in Symja #454
TiagoCavalcante
started this conversation in
Ideas
Replies: 1 comment 2 replies
-
A first starting point can be to integrate existing Satisfiability modulo theories: An umbrella project for the different solvers seems to be "JavaSMT - Unified Java API for SMT solvers.": For boolean logic the "LogicNG" project is already used in Symja as a dependency: See |
Beta Was this translation helpful? Give feedback.
2 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
The [few] proof assistants available in the "market" (all I know are free, and probably all that exists are free, as they won't have [m]any buyers).
Proof assistants aren't used widely mostly because their syntax is weird, and they have a steep learning curve.
WL (and Symja, and Mathics) have a syntax that is easier to use on the other hand. After searching I have found that [almost?] nobody uses WL for proof assistant, probably because it doesn't support it. And so I had the idea: can a proof assistant be developed in Symja?
The core of a proof assistant is to follow logical steps, and check if their logic is correct based on a set of axioms (axioms like ∀x,y . ∀z (z ∈ x ∧ z ∈ y) ⟺ x = y or 1+1=2).
I think that a library could provide functions that receive assumptions and logical expressions, and check if every step makes sense.
An idea of how it would be:
This is just an idea and probably my "design" can be improved by 100%.
If a good "design" is created, I'd like to help to implement it.
Beta Was this translation helpful? Give feedback.
All reactions