| README.md | ||
Introduction
Liblogic is a library of functions and data structures which together aim to provide access to the tools and conventions of formal logic. It came to be out of the need to quickly test axiomatic systems and make automated discoveries, as is the case with any proof assistant, with the distinction that liblogic aims to be generic so that it is an indispensable tool for any logician desirous of algorithmic evaluation of logical problems.
In essence, all proof assistants have within them something like liblogic, and so as to reduce the need for boilerplate in future endeavours, liblogic aims to provide for the needs of any proof assistant or similar program, spare the details involved in the specific user interface.
Seeing as one of the major goals of the project is the automated discovery of truths in a given axiomatic system, it is imperative that the algorithms used be highly optimised so as to enable massive concurrent computation of such systems to the greatest possible degree.
Goals
Given that the project is in its infancy, the following goals are what would constitute the minimum viable product. In the long term the project ought to take optimisation and generalisation as its chief purposes, but for now the following are needed to simply get it off the ground:
- Ability to validate or invalidate arbitrary arguments of truth‐functional logic
- Ability to evaluate any arbitrary group of truth‐functional propositions as being either contradictory, contingent, or tautological
- Ability to prune from a group of propositions those which are tautologies and those which follow from the others
As seen, at the moment the project concerns itself strictly with truth‐functional logic, but the hope is that in the future the project will expand to accommodate more expressive logics such as first order logic, modal logic, and eventually higher order logics. If at all possible, it is desirable to facilitate the definition of arbitrary logics such that the core suite of functions will still operate correctly on these logics, but that is a problem for future contributors to consider.