You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
Theorem Proving for All Equational Reasoning in Liquid Haskell Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton [PDF] 1.Introduction 2.Reasoning about Programs 2.1. Lightweight Reasoning 2.2. Induction on Lists 2.3. Proof Automation 3.Totality and Termination 3.1. Totality Checking 3.2. Termination Checking 3.3. Uncaught termination 4.Function Optimization 4.1. Example:
The Qiita Advent Calendar 2017 is supported by the following companies, organizations, and services.
« Field Notes on the Behaviour of a Large Assemblage of Ecologists | Main | Globular for Higher-Dimensional Knottings (Part 2) » guest post by Scott Carter About 7 months ago, Jamie Vicary contacted me with a Globular worksheet of which, initially, I could make neither heads nor tails. He patiently explained to me that what I was looking at was an example that I had worked out for Bruce Bartlett o
Mizarの処理系はまったく使いにくいです。その使い勝手は極悪ですわ。それにも関わらず僕が我慢して使おうとしているのは、Mizarの構文と意味モデルが素晴らしいからです。最高ですわ。特に、他の証明系のタクティク言語の難読さに辟易した人には感激もんです。 「証明検証系Mizarを試してみる」で例に出した次の証明記述コードを例にします。 reserve i,j,k,l,m,n for natural number; i+k = j+k implies i=j; proof defpred P[natural number] means i+$1 = j+$1 implies i=j; A1: P[0] proof assume B0: i+0 = j+0; B1: i+0 = i by INDUCT:3; B2: j+0 = j by INDUCT:3; hence thesis by B0,
This is the web site for the early stages of a book introducing both machine-checked proof with the Coq proof assistant and approaches to formal reasoning about program correctness. Grab a Draft Source on GitHub Quasi-latest PDF draft Quasi-latest source-code tarball Quasi-latest source-code tarball, library only (warning: the author really does not recommend using it in serious projects!) Use in
この記事はTheorem Prover Advent Calendarの22日めの担当記事です. 今年の僕の持ちネタの一つですが,ipc_bot というTwitter botを作りました. https://twitter.com/ipc_bot このbotは直観主義命題論理の命題を投げると解いてくれるbotです. 仕組み 証明を探すのは適当にやっても出来るのですが,証明が存在しないことを確認するのは結構大変です. (古典論理の場合は与えられた命題の否定をSATソルバーにかければ正誤がわかりますが,直観主義論理命題論理だとそう簡単ではありません) 証明が存在するかどうかを有限時間内で判定するには,推論規則を色々いじる必要があります.しかしその説明をはてなブログで書くのが面倒になってしまったので過去に某所に寄稿したものを見て下さい. http://www.tsg.ne.jp/buho/305/
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く