Ещё в тему есть CLI штука на питоне theorem-prover. Как будто о том же самом, но уже чуть понятнее. Тут производится автоматическая проверка истинности логического высказывания. Есть тонкости с введением собственных аксиом, но в общем примерно так. Ну то есть, P or not P истинно для любого P, а P and not P ложно для любого P, что эта штука, собственно, и вычисляет.