theorem-proving

5calore

1risposta

In lotta con la tattica della riscrittura in Idris

Sto esaminando il vero libro di analisi di Terry Tao, che costruisce la matematica fondamentale dai numeri naturali in su. Formulando quante più prove possibili, spero di familiarizzare con Idris e ti

5calore

1risposta

Idris ha un equivalente alle espressioni `_` di Agda?

Oltre ad avere argomenti impliciti, Agda consente di omettere il valore di un argomento esplicito e sostituirlo con una metavariabile, indicata dal carattere _, il cui valore viene quindi determinato

6calore

1risposta

formule di risolutore interno in z3

Lo strumento di dimostrazione del teorema z3 impiega molto tempo per risolvere una formula, che ritengo dovrebbe essere in grado di gestire facilmente. Per capire meglio e possibilmente ottimizzare il

19calore

1risposta

Limiti di risolutori SMT

Tradizionalmente la maggior parte del lavoro con la logica computazionale era proposizionale, nel qual caso si utilizzava un solutore SAT (soddisfacibilità booleana) o di primo ordine, nel qual caso s

5calore

1risposta

Coq non è in grado di trovare sottotermine quando si utilizza la tattica di riscrittura

Sto provando a eseguire una prova modificata di compile_correct da first chapter di Programmazione certificata con tipi dipendenti. Nella mia versione, cerco di far uso del fatto che progDenote è una

26calore

2risposta

Come imparare agda

Sto cercando di imparare agda. Tuttavia, ho avuto un problema. Tutti i tutorial che ho trovato su agda wiki sono troppo complessi per me e riguardano diversi aspetti della programmazione. Dopo la lett

5calore

2risposta

Come implementare la logica Horn pienamente dichiarativa?

Vorrei formalizzare alcune conoscenze ed eseguire query in quello che può essere definito come completamente dichiarativo Horn logic (o Prologo pienamente dichiarativo). Qualcuno potrebbe fornire alcu

7calore

1risposta

Come implementare l'algoritmo Hare e Tortoise di Floyd in Agda?

Voglio tradurre il seguente codice Haskell in Agda: import Control.Arrow (first) import Control.Monad (join) safeTail :: [a] -> [a] safeTail [] = [] safeTail (_:xs) = xs floyd :: [a] -> [a] ->

18calore

1risposta

Z3: trovare tutti i modelli soddisfacenti

Sto cercando di recuperare tutti i possibili modelli per alcune teorie del primo ordine usando Z3, un risolutore SMT sviluppato da Microsoft Research. Ecco un esempio di lavoro minima: (declare-const

6calore

1risposta

Invocazione di Nitpick e Sledgehammer insieme in Isabelle

Quando dichiaro un lemma in Isabelle, spesso digito nitpick e, se questo non mi dà un controesempio. Quindi digitare sledgehammer per provare a trovare automaticamente una prova. mi chiedo: è possibil