theorem-proving

5Hitze

1Antwort

Kämpfen mit Rewrite-Taktik in Idris

Ich gehe durch Terry Taos echtes Analyse-Lehrbuch, das grundlegende Mathematik von den natürlichen Zahlen aufbaut. Indem ich so viele Beweise wie möglich formalisiere, hoffe ich, mich sowohl mit Idris

dependent-type idris theorem-proving 2016-06-16

---

5Hitze

1Antwort

Hat Idris ein Äquivalent zu Agdas `_` Ausdrücken?

Zusätzlich zu impliziten Argumenten können Sie mit Agda den Wert eines expliziten Arguments weglassen und durch eine Metavariable ersetzen, die mit dem Zeichen _ gekennzeichnet ist und deren Wert dann

agda dependent-type theorem-proving idris 2016-03-10

---

4Hitze

3Antwort

Beweise über Funktionen, die von der Reihenfolge ihrer Alternativen abhängen

Mit einiger Erfahrung in Haskell, habe ich gerade angefangen, Idris für Theoremprüfung zu verwenden. Dies ist ein minimales Beispiel, das ein Problem veranschaulicht, das ich beim Versuch, ziemlich ei

pattern-matching dependent-type idris theorem-proving 2016-06-29

---

2Hitze

1Antwort

Gibt es eine Möglichkeit, SMT-Solver zu verwenden, um herauszufinden, wie Funktionen zusammengesetzt werden?

Ich bin ein Anfänger zu SMT-Lösern und ich versuche, sie für eine Variation der Programmsynthese zu verwenden. Wie auch immer, worauf das Problem hinausläuft, ist eine Folge von angewandten Operatione

z3 smt theorem-proving 2016-05-14

---

0Hitze

1Antwort

Isabelle Buch Übung 2.11: Ausdrücke Polynom Form Transforming

meine Frage bezüglich Übung 2.11 in dem Buch Beton Semantics (http://concrete-semantics.org/): arithmetische Ausdrücke in einer Variablen über ganze Zahlen definieren (Typ int) als Datentyp: datatype

isabelle theorem-proving 2016-05-16

---

7Hitze

1Antwort

Coq simpl für Programm Fixpunkt

Gibt es etwas wie die Taktik simpl für Program Fixpoint s? Insbesondere, wie kann man die folgende triviale Aussage beweisen? Program Fixpoint bla (n:nat) {measure n} := match n with | 0 => 0 | S n

coq theorem-proving totality 2016-03-31

---

4Hitze

1Antwort

Unterschied zwischen Logikprogrammierung und automatisiertem Theorembeweis

Was ist der Unterschied zwischen Logikprogrammierung und automatisiertem Theorembeweis (ATP) (z. B. mit E-Prover, Spass oder Princess)? Ich suchte viel und die einzige Information, die ich fand, ist,

prolog theorem-proving logic-programming 2016-03-31

---

7Hitze

1Antwort

Wie implementiert man Floyds Hare and Tortoise-Algorithmus in Agda?

Ich möchte folgendes Haskell-Code in Agda übersetzen: us import Control.Arrow (first) import Control.Monad (join) safeTail :: [a] -> [a] safeTail [] = [] safeTail (_:xs) = xs floyd :: [a] -> [

haskell functional-programming agda theorem-proving floyd-cycle-finding 2016-02-17

---

5Hitze

2Antwort

Isabelle2016 und Proof General

Ich habe versucht, Isabelle 2016 zu lernen. Während ich grundsätzlich die Idee der asynchronen Proofüberprüfung mag, mag ich Isabelle/jEdit nicht aus einer Reihe von Gründen, von denen die schwerwiege

isabelle theorem-proving proof-general 2016-02-21

---

1Hitze

1Antwort

Warum kann Z3 nicht beweisen/zugeben, dass `is_int` bei einigen Operationen geschlossen ist?

Zum Beispiel der folgenden Abfrage mal aus: (declare-const x Real) (declare-const y Real) (assert (is_int x)) (assert (is_int y)) (assert (not (is_int (+ x y)))) (check-sat) Soweit ich, die Z3

z3 smt theorem-proving 2016-06-03

---