Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 19-Jan-2021 10:10:18 JST きゅーけー

   Guile で動く定理証明支援系を作った。だいたい自分の望むものは手に入ったので、とりあえずはこれを使って『定理証明手習い』を一周してみようと思う。

   https://gitlab.com/tojoqk/vikalpa

   • sumiyaki likes this.
   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 19-Jan-2021 10:26:05 JST きゅーけー

     in reply to

     まだドキュメントはないので使い方を把握するのは困難な状況なのですが、下記で append の結合性の証明をしているのでなんとなく何をやっているのかは把握できるかもと思ってます。

     https://gitlab.com/tojoqk/vikalpa/-/blob/f5879492135a41edd1f227607dcbc8d0c25c5c3c/tests/test-vikalpa.scm#L346