theorem-proving

2熱

1答えて

Coqでアサートを許可する方法はありますか？は、私はこのような定理があるとします。 Theorem test : forall m n : nat, m * n = n * m. Proof. intros n m. assert (H1: m + m * n = m * S n). { Admitted. } Abort. 上記のassertが私のために動

-1熱

1答えて

FOLモデルの一貫性チェック

私はFirst Orderロジックでモデルを開発しています。私はそれが一貫していることを証明したいと思います。出来ますか？これを行うために私が使用できる無料のツールはありますか？これはGodel定理のために不可能ですか？よろしくお願いいたします。

3熱

1答えて

選択モナドが応用モナドであることをCoq証明する

私はcoqにはかなり新しく、これまで手で証明できるものだけを証明することができました。ですからセレクションモナドを見て、それをインテルで実装しようと思ったとき、それは良いエクササイズになると思ったが、私は立ち往生した。誰かが、選択モナドが応用的でモナドであるという証拠の例をcoqで提供することができますか？ここにfunkのhaskell実装があります。 newtype Sel r a = Sel

1熱

1答えて

コックは、以下に示すように、私は次の定理に解決策を与えた誘導仮説

を生成しない： Require Import Coq.Lists.List. Import ListNotations. Inductive suffix {X : Type} : list X -> list X -> Prop := | suffix_end : forall xs, suffix xs xs | suffix_step : forall

1熱

1答えて

式トランスレータを定義する方法は？

私は2つのほとんど同じ言語（fooとbar）に定義： theory SimpTr imports Main begin type_synonym vname = "string" type_synonym 'a env = "vname ⇒ 'a option" datatype foo_exp = FooBConst bool | FooIConst i

1熱

1答えて

どのようにプロップのパターンマッチをするタイプ

に排除することなく、コックに証明するとき、私はソートされたリストの末尾ではなく戦術のパターンマッチングを使用して、コックにソートされていることを証明しようとしている： Require Import Coq.Sorting.Sorted. Definition tail_also_sorted {A : Prop} {R : relation A} {h : A} {t : list A}

1熱

1答えて

Agdaにおける決定的な平等はn^2未満の場合？

私は推論したいプログラミングランゲージのASTのデータ型を持っていますが、ASTのコンストラクタは約10種類あります。 data Term : Set where UnitTerm : Term VarTerm : Var -> Term ... SeqTerm : Term -> Term -> Term 私は、この言語の構文木のために決定的な平等性を

1熱

1答えて

TPTPの文法的に異なる用語を表現する

私はVampireやE-Proverのような一次論理定理証明者を見ています.TPTP構文は今後の道のりです。 Answer Set ProgrammingとPrologのようなLogic Programmingの構文にはよく慣れていますが、TPTP syntaxの詳細な説明を参照しようとしていますが、解釈されたファンクタと解釈されないファンクタを正しく区別する方法はまだ分かりません。間違った用語を

0熱

1答えて

無限反転ループCoq

私は以下に示す接尾辞のような誘導関係を持っています。私は関連する定理を証明しようとしています suffix_app。私の一般的なアイデアは、xsがysと等しいか、それが何らかの一連の要素であることを示すために接尾辞xs ysというその事実を使用することです。 cons ' Require Import Coq.Lists.List. Import ListNotations. Inducti