Package: minlog (4.0.99.20100221-6)

[ Source: minlog  ]

assistente per dimostrazioni basato su calcolo deduttivo naturale del primo ordine

Pensato per ragionare su funzioni calcolabili, usando una logica minimale invece della logica classica o intuizionista. La principale motivazione alla base di MINLOG è di sfruttare il paradigma delle dimostrazioni-come-programmi per lo sviluppo e la verifica dei programmi. Le dimostrazioni sono di fatto trattate come oggetti di prima classe che possono essere normalizzati. Se una formula è esistenziale, allora la sua dimostrazione può essere usata per leggere una sua istanza o essere cambiata in modo appropriato per lo sviluppo di programmi grazie ad una trasformazione della dimostrazione. A questo scopo MINLOG è fornito di strumenti per estrarre programmi funzionali direttamente dai termini della dimostrazione. Questo è vero anche per le dimostrazioni non costruttive, usando una traduzione-A raffinata. Il sistema è supportato dalla ricerca e normalizzazione automatiche di dimostrazioni via valutazione, come un dispositivo efficace di riscrittura dei termini.

Minlog può essere usato con ProofGeneral che permette di modificare le dimostrazioni usando emacs e xemacs. Ciò richiede l'installazione del pacchetto proofgeneral-minlog.

Other Packages Related to minlog

• dep: racket

  linguaggio di programmazione estensibile nella famiglia Scheme

  or guile

  virtual package provided by guile-2.0, guile-2.2

• rec: emacs25

  pacchetto di transizione a emacs-gtk di GNU Emacs

  or emacs24

  pacchetto di transizione a emacs-gtk di GNU Emacs

  or emacsen

  virtual package provided by emacs-gtk, emacs-lucid, emacs-nox, xemacs21-mule, xemacs21-mule-canna-wnn, xemacs21-nomule

• sug: proofgeneral-minlog

  Package not available

• sug: quack-el

  Package not available

Download minlog

Download for all available architectures

Architecture	Package Size	Installed Size	Files
all	2,568.0 kB	7,555.0 kB	[list of files]