FindEquationalProof

FindEquationalProof[thm,axms]

tries to find a proof of the equational logic theorem thm using the axioms axms.

FindEquationalProof[thm,"theory"]

tries to find a proof of thm using the specified named axiomatic theory.

Details and Options

Examples

open all close all

Basic Examples  (2)

Prove an elementary theorem in propositional logic:

In[1]:=
Click for copyable input
Out[1]=

Show the abstract proof network:

In[2]:=
Click for copyable input
Out[2]=

Show the complete list of proof steps as a Dataset object:

In[3]:=
Click for copyable input
Out[3]=

Prove a theorem involving universal quantification in first-order logic:

In[1]:=
Click for copyable input
Out[1]=

Typeset a natural language argument:

In[2]:=
Click for copyable input
Out[2]=

Build a function that performs the steps of the proof:

In[3]:=
Click for copyable input
Out[3]=
In[4]:=
Click for copyable input
Out[4]=

Scope  (2)

Options  (1)

Applications  (11)

Properties & Relations  (2)

Possible Issues  (1)

Introduced in 2018
(11.3)
|
Updated in 2019
(12.0)