厨房程度の証明をパソコンで計算させたいです。
世の中には電卓やmathematicaがあるので他の計算はパソコンで出来ますが
証明はどうやら今の所パソコンにうまく移植出来ていないみたいです。
よって証明をパソコンにやらせようと考えたっていいじゃない?
以下、雛形。

入力:仮定
input:Given
出力:結論
output:Definition
図:ネットリスト
Figure:netlist
証明:rawfile
Proof:rawfile

cf.)電子回路シミュレータSpice

l//mならば、∠a=∠b
∠a=∠bならば、l//m

Parallel lines l and m, and a line q which intersects both l and m (Reasons:Given)
angle(a) and angle(b) are corresponding angles.

angle(a)=angle(b)

parallel_line(l),parallel_line(m) (Reasons:Given)
angle(a)=angle(b)

angle(a)=angle(b) (Reason:Given)
parallel_line(l),parallel_line(m)

input
[netlist]
parallel_line l a
parallel_line m b
intersect_line q a b

output
[rawfile]
angle(a)=angle(b)

a//b,a//cならば、b//c

If parallel_lineS(a,b) and parallel_lineS(a,c) (Reasons:Given)
parallel_line(b),parallel_line(c).

[netlist]
parallel_lineS a b
parallel_lineS a c

[rawfile]
parallel_lineS b c

メールはこちらまで