minlog_4.0.99.20100221-5.2_all.deb


Advertisement

Description

minlog - Proof assistant based on first order natural deduction calculus

Property Value
Distribution Ubuntu 12.04 LTS (Precise Pangolin)
Repository Ubuntu Universe amd64
Package name minlog
Package version 4.0.99.20100221
Package release 5.2
Package architecture all
Package type deb
Installed size 8.39 KB
Download size 2.75 MB
Official Mirror archive.ubuntu.com
intended to reason about computable functionals, using minimal
rather than classical or intuitionistic logic. The main motivation
behind MINLOG is to exploit the proofs-as-programs paradigm for
program development and program verification. Proofs are in fact
treated as first class objects which can be normalized. If a formula
is existential then its proof can be used for reading off an instance
of it, or changed appropriately for program development by proof
transformation. To this end MINLOG is equipped with tools to extract
functional programs directly from proof terms. This also applies to
non-constructive proofs, using a refined A-translation. The system
is supported by automatic proof search and normalization by
evaluation as an efficient term rewriting device.
Minlog can be used with ProofGeneral, which allows proofs to be
edited using emacs and xemacs. This requires the proofgeneral-minlog
package to be installed.

Alternatives

Package Version Architecture Repository
minlog_4.0.99.20100221-5.2_all.deb 4.0.99.20100221 all Ubuntu Universe
minlog - - -

Requires

Name Value
guile -
plt-scheme -

Download

Type URL
Binary Package minlog_4.0.99.20100221-5.2_all.deb
Source Package minlog

Install Howto

  1. Update the package index:
    # sudo apt-get update
  2. Install minlog deb package:
    # sudo apt-get install minlog

Files

Path
/usr/bin/minlog
/usr/share/doc-base/minlog
/usr/share/doc/minlog/changelog.Debian.gz
/usr/share/doc/minlog/copyright
/usr/share/doc/minlog/mlcf.pdf
/usr/share/doc/minlog/mpcref.pdf
/usr/share/doc/minlog/ref.pdf
/usr/share/doc/minlog/reflection_manual.pdf
/usr/share/doc/minlog/tutor.pdf
/usr/share/doc/minlog/examples/Makefile
/usr/share/doc/minlog/examples/Makefile.template
/usr/share/doc/minlog/examples/reflection.scm
/usr/share/doc/minlog/examples/test.save
/usr/share/doc/minlog/examples/test.scm
/usr/share/doc/minlog/examples/tutorial.scm
/usr/share/doc/minlog/examples/warning.txt
/usr/share/doc/minlog/examples/Schueler/germanise.scm
/usr/share/doc/minlog/examples/Schueler/probestud.scm
/usr/share/doc/minlog/examples/Schueler/probestudstart.scm
/usr/share/doc/minlog/examples/analysis/cont.scm
/usr/share/doc/minlog/examples/analysis/extraction.scm
/usr/share/doc/minlog/examples/analysis/real.scm
/usr/share/doc/minlog/examples/analysis/simpreal.scm
/usr/share/doc/minlog/examples/arith/Makefile
/usr/share/doc/minlog/examples/arith/bundeswett.scm
/usr/share/doc/minlog/examples/arith/realsqrttwo.scm
/usr/share/doc/minlog/examples/arith/sqrttwo.scm
/usr/share/doc/minlog/examples/arith/quotrem/Makefile
/usr/share/doc/minlog/examples/arith/quotrem/pair.tac
/usr/share/doc/minlog/examples/arith/quotrem/quotrem-ex.save
/usr/share/doc/minlog/examples/arith/quotrem/quotrem-ex.scm
/usr/share/doc/minlog/examples/bar/Makefile
/usr/share/doc/minlog/examples/bar/bar.save
/usr/share/doc/minlog/examples/bar/bar.scm
/usr/share/doc/minlog/examples/bar/higman-finite.scm
/usr/share/doc/minlog/examples/bar/higman01.save
/usr/share/doc/minlog/examples/bar/higman01.scm
/usr/share/doc/minlog/examples/classical/Makefile
/usr/share/doc/minlog/examples/classical/hsh.scm
/usr/share/doc/minlog/examples/classical/root.save
/usr/share/doc/minlog/examples/classical/root.scm
/usr/share/doc/minlog/examples/classical/surj.scm
/usr/share/doc/minlog/examples/classical/wftest.save
/usr/share/doc/minlog/examples/classical/wftest.scm
/usr/share/doc/minlog/examples/classical/combinatorics/booleantape.scm
/usr/share/doc/minlog/examples/classical/combinatorics/pigeonhole.scm
/usr/share/doc/minlog/examples/classical/combinatorics/tape.scm
/usr/share/doc/minlog/examples/classical/dickson/dickson.tac
/usr/share/doc/minlog/examples/classical/dickson/dickson2gen.scm
/usr/share/doc/minlog/examples/classical/dickson/dickson_gen.scm
/usr/share/doc/minlog/examples/classical/dickson/dickson_lemma1.scm
/usr/share/doc/minlog/examples/classical/dickson/dickson_lemma2.scm
/usr/share/doc/minlog/examples/classical/gcd/gcd-a.scm
/usr/share/doc/minlog/examples/classical/gcd/gcd-d.scm
/usr/share/doc/minlog/examples/classical/gcd/gcd-gind.scm
/usr/share/doc/minlog/examples/classical/gcd/gcd.scm
/usr/share/doc/minlog/examples/classical/gcd/gcd_minpr.scm
/usr/share/doc/minlog/examples/dc/Makefile
/usr/share/doc/minlog/examples/dc/dc-first.save
/usr/share/doc/minlog/examples/dc/dc-first.scm
/usr/share/doc/minlog/examples/diatup/BinTape.scm
/usr/share/doc/minlog/examples/diatup/BinTapeBis.scm
/usr/share/doc/minlog/examples/diatup/DicksonTwo.scm
/usr/share/doc/minlog/examples/diatup/IndZeroTest.scm
/usr/share/doc/minlog/examples/diatup/IntegerRoot.scm
/usr/share/doc/minlog/examples/diatup/NonExStabTest.scm
/usr/share/doc/minlog/examples/diatup/TytupAssoc.scm
/usr/share/doc/minlog/examples/diatup/hsh-Berger.scm
/usr/share/doc/minlog/examples/diatup/HeredExtEq/DoubleSum.scm
/usr/share/doc/minlog/examples/diatup/HeredExtEq/SimpleSum.scm
/usr/share/doc/minlog/examples/diatup/HeredExtEq/TripleSum.scm
/usr/share/doc/minlog/examples/diatup/HeredExtEq/heeq-def.scm
/usr/share/doc/minlog/examples/diatup/IndAxiom/IND-exall.scm
/usr/share/doc/minlog/examples/diatup/IndAxiom/IND-pureEx.scm
/usr/share/doc/minlog/examples/diatup/IndAxiom/IND-qfr.scm
/usr/share/doc/minlog/examples/diatup/IndAxiom/IndAxSrc.scm
/usr/share/doc/minlog/examples/diatup/fibonacci/fib-ATR.scm
/usr/share/doc/minlog/examples/diatup/fibonacci/fib-DIA.scm
/usr/share/doc/minlog/examples/diatup/fibonacci/newatr.scm
/usr/share/doc/minlog/examples/dijkstra/Makefile
/usr/share/doc/minlog/examples/dijkstra/count.save
/usr/share/doc/minlog/examples/dijkstra/count.scm
/usr/share/doc/minlog/examples/dijkstra/dijkstra.save
/usr/share/doc/minlog/examples/dijkstra/dijkstra.scm
/usr/share/doc/minlog/examples/dijkstra/example.scm
/usr/share/doc/minlog/examples/dijkstra/pick.scm
/usr/share/doc/minlog/examples/dijkstra/wf.scm
/usr/share/doc/minlog/examples/fan/fanwklu.scm
/usr/share/doc/minlog/examples/fibonacci/equal-add.mpc
/usr/share/doc/minlog/examples/fibonacci/fib-functional.mpc
/usr/share/doc/minlog/examples/fibonacci/fib.mpc
/usr/share/doc/minlog/examples/fibonacci/fib.scm
/usr/share/doc/minlog/examples/fibonacci/fibconstr.scm
/usr/share/doc/minlog/examples/hounif/Makefile
/usr/share/doc/minlog/examples/hounif/nipkow.save
/usr/share/doc/minlog/examples/hounif/nipkow.scm
/usr/share/doc/minlog/examples/hounif/nipkow.tac
/usr/share/doc/minlog/examples/mpc/list1.mpc
/usr/share/doc/minlog/examples/mpc/list2.mpc
/usr/share/doc/minlog/examples/mpc/nat0.scm
/usr/share/doc/minlog/examples/mpc/nat1.mpc
/usr/share/doc/minlog/examples/mpc/nat1.scm
/usr/share/doc/minlog/examples/mpc/nat2.mpc
/usr/share/doc/minlog/examples/mpc/nat2.scm
/usr/share/doc/minlog/examples/mpc/nat3.mpc
/usr/share/doc/minlog/examples/mpc/nat3.scm
/usr/share/doc/minlog/examples/mpc/nat4.mpc
/usr/share/doc/minlog/examples/mpc/nat4.scm
/usr/share/doc/minlog/examples/mpc/prop.mpc
/usr/share/doc/minlog/examples/mpc/quant.mpc
/usr/share/doc/minlog/examples/mpc/quant1.mpc
/usr/share/doc/minlog/examples/mpc/quant1.scm
/usr/share/doc/minlog/examples/mpc/quant2.mpc
/usr/share/doc/minlog/examples/mpc/quant2.scm
/usr/share/doc/minlog/examples/mpc/quant3.mpc
/usr/share/doc/minlog/examples/mpc/quant3.scm
/usr/share/doc/minlog/examples/normtest/normtest.scm
/usr/share/doc/minlog/examples/ordinals/boolean.scm
/usr/share/doc/minlog/examples/ordinals/e0.zip
/usr/share/doc/minlog/examples/ordinals/hao.scm
/usr/share/doc/minlog/examples/ordinals/hao_cnf.scm
/usr/share/doc/minlog/examples/ordinals/hao_relations.scm
/usr/share/doc/minlog/examples/ordinals/hao_suc.scm
/usr/share/doc/minlog/examples/ordinals/hao_term.scm
/usr/share/doc/minlog/examples/ordinals/nat.scm
/usr/share/doc/minlog/examples/ordinals/natnum.scm
/usr/share/doc/minlog/examples/ordinals/ordinals.scm
/usr/share/doc/minlog/examples/ordinals/pao.zip
/usr/share/doc/minlog/examples/ordinals/reflection.scm
/usr/share/doc/minlog/examples/ordinals/reflection_alpha.scm
/usr/share/doc/minlog/examples/ordinals/reflection_nat.scm
/usr/share/doc/minlog/examples/ordinals/reflection_numbers.scm
/usr/share/doc/minlog/examples/ordinals/reflection_numbers_thms.scm
/usr/share/doc/minlog/examples/ordinals/reflection_rationals.scm
/usr/share/doc/minlog/examples/ordinals/reflection_thms.scm
/usr/share/doc/minlog/examples/ordinals/ring.scm
/usr/share/doc/minlog/examples/ordinals/FAN/bar.scm
/usr/share/doc/minlog/examples/ordinals/FAN/positive.scm
/usr/share/doc/minlog/examples/ordinals/FAN/ucomp.scm
/usr/share/doc/minlog/examples/ordinals/FAN/wklfan.scm
/usr/share/doc/minlog/examples/prop/Makefile
/usr/share/doc/minlog/examples/prop/prop.save
/usr/share/doc/minlog/examples/prop/prop.scm
/usr/share/doc/minlog/examples/pruning/align.scm
/usr/share/doc/minlog/examples/pruning/maxseg.scm
/usr/share/doc/minlog/examples/quant/Makefile
/usr/share/doc/minlog/examples/quant/README
/usr/share/doc/minlog/examples/quant/hofmann.save
/usr/share/doc/minlog/examples/quant/hofmann.scm
/usr/share/doc/minlog/examples/quant/lnf.save
/usr/share/doc/minlog/examples/quant/lnf.scm
/usr/share/doc/minlog/examples/quant/los.scm
/usr/share/doc/minlog/examples/quant/orevkov.save
/usr/share/doc/minlog/examples/quant/orevkov.scm
/usr/share/doc/minlog/examples/quant/quant.save
/usr/share/doc/minlog/examples/quant/quant.scm
/usr/share/doc/minlog/examples/tait/dbrealrs.scm
/usr/share/doc/minlog/examples/tait/sn.scm
/usr/share/doc/minlog/examples/tait/taitRun.scm
/usr/share/doc/minlog/examples/tait/taitScott.scm
/usr/share/doc/minlog/examples/tait/taitScottPartial.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/Lem1.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/Lem2.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/Lem3.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/NT.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/README.txt
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/auxGlobal.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/auxGlobal_SHORT.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/auxLem1.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/auxLem1_SHORT.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/auxLem3.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/auxLem3_SHORT.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/auxNT.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/auxNT_SHORT.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/auxSC.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/defsAxioms.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/defsAxiomsSpecial.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/defsLamCalc.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/defsNT.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/defsPred.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/defsSubst.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/initiate.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/omega.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/proofAxiomsGlobal.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/proofAxiomsGlobal_SHORT.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/proofAxiomsPart1.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/proofAxiomsPart2.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/subst_Joachimski.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/subst_Joachimski_SHORT.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/tait.scm
/usr/share/doc/minlog/examples/tait/diplomarbeit_schlenker/trivial.scm
/usr/share/doc/minlog/examples/train/index.scm
/usr/share/doc/minlog/examples/train/index2int.scm
/usr/share/doc/minlog/examples/train/int.scm
/usr/share/doc/minlog/examples/train/pos.scm
/usr/share/doc/minlog/examples/train/train.scm
/usr/share/doc/minlog/examples/warshall/Makefile
/usr/share/doc/minlog/examples/warshall/lemmas.mpc
/usr/share/doc/minlog/examples/warshall/warshall.mpc
/usr/share/doc/minlog/examples/warshall/warshall.save
/usr/share/doc/minlog/examples/warshall/warshall.scm
/usr/share/emacs/site-lisp/minlog/minlog-mode.el
/usr/share/emacs/site-lisp/minlog/minlog.el
/usr/share/man/man1/minlog.1.gz
/usr/share/minlog/init.scm
/usr/share/minlog/lib/exc.scm
/usr/share/minlog/lib/list.scm
/usr/share/minlog/lib/listrev.scm
/usr/share/minlog/lib/minpr.scm
/usr/share/minlog/lib/minpr_gen.scm
/usr/share/minlog/lib/nat.scm
/usr/share/minlog/lib/nat2.scm
/usr/share/minlog/lib/natinf.scm
/usr/share/minlog/lib/numbers.scm
/usr/share/minlog/lib/realsimp.scm
/usr/share/minlog/lib/tensor.scm
/usr/share/minlog/lib/tsil.scm
/usr/share/minlog/modules/diatup.scm
/usr/share/minlog/modules/type-inf.scm
/usr/share/minlog/src/atr.scm
/usr/share/minlog/src/axiom.scm
/usr/share/minlog/src/boole.scm
/usr/share/minlog/src/ets.scm
/usr/share/minlog/src/etsd.scm
/usr/share/minlog/src/formula.scm
/usr/share/minlog/src/gen-app.scm
/usr/share/minlog/src/grammar.scm
/usr/share/minlog/src/init.scm
/usr/share/minlog/src/lalr.scm
/usr/share/minlog/src/list.scm
/usr/share/minlog/src/lnf.scm
/usr/share/minlog/src/logical.scm
/usr/share/minlog/src/lr-dvr.scm
/usr/share/minlog/src/minitab.scm
/usr/share/minlog/src/mpc.scm
/usr/share/minlog/src/pconst.scm
/usr/share/minlog/src/pp-sexp.scm
/usr/share/minlog/src/pp.scm
/usr/share/minlog/src/pproof.scm
/usr/share/minlog/src/prologue.scm
/usr/share/minlog/src/proof.scm
/usr/share/minlog/src/prop.scm
/usr/share/minlog/src/psym.scm
/usr/share/minlog/src/run-mpc.scm
/usr/share/minlog/src/term.scm
/usr/share/minlog/src/todo.scm
/usr/share/minlog/src/typ.scm
/usr/share/minlog/src/unicode.scm
/usr/share/minlog/src/var.scm
/usr/share/minlog/src/welcome.scm

Changelog

2010-07-17 - gregor herrmann <gregoa@debian.org>
minlog (4.0.99.20100221-5.2) unstable; urgency=low
* Non-maintainer upload.
* Fix "contains /usr/share/doc-base/doc-base":
s/doc-base/minlog/ debian/minlog.doc-base
(closes: #581738).
2010-05-11 - Jari Aalto <jari.aalto@cante.net>
minlog (4.0.99.20100221-5.1) unstable; urgency=low
[ Jari Aalto ]
* Non-maintainer upload.
- Move to packaging format "3.0 (quilt)" due to patch.
* debian/compat
- Update to 7.
* debian/control
- Remove EOL whitespaces.
- (Build-Depends): Change obsolete mzscheme to plt-scheme.
Patch tanks to Hideki Yamane (Debian-JP) <henrich@debian.or.jp>
(FTBFS; Closes: #577343). Add emacs23. Remove emacs21.
Update to debhelper 7.1.
- (Depends): Add ${misc:Depends}.
- (Homepage): New field.
- (Standards-Version): Update to 3.8.4.
* debian/copyright
- Update old FSF addresses to point to URL.
- Point to GPL-2. Remove EOL whitespaces.
* debian/doc-base
- New file.
* debian/rules
- Remove EOL whitespaces.
- (install): Update dh_clean to dh_prep.
* debian/source/format
- New file.
* debian/watch
- New file.
2010-02-20 - Freiric Barral <barral@math.lmu.de>
minlog (4.0.99.20100221-5) unstable; urgency=low (high for users of mzsccheme)
* Closes: #570235 due to incompatibility between mzscheme and r5rs
* upate to svn head
2010-02-13 - Christoph Egger <christoph@debian.org>
minlog (4.0.99.20080304-4.1) unstable; urgency=low
* Non-maintainer upload.
* add ${misc:Depends}
* Change Build dependency fronm tetex to texlive (Closes: #562301)
2008-03-04 - Freiric Barral <barral@math.lmu.de>
minlog (4.0.99.20080304-4) unstable; urgency=low
* CVS snapshot
2007-10-12 - Freiric Barral <barral@math.lmu.de>
minlog (4.0.99-4) unstable; urgency=low
* Added missing copyright notices.
* Initial upload closes: #406186
2006-11-03 - Freiric Barral <barral@math.lmu.de>
minlog (4.0.99-3) unstable; urgency=low
* XEmacs does not work with Minlog. So recommend either emacs21 or
emacs22 (though the latter is not available yet).
2006-11-02 - Freiric Barral <barral@math.lmu.de>
minlog (4.0.99-2) unstable; urgency=low
* Use debhelper v4 and therefore put everything into debian/minlog
2006-11-01 - Freiric Barral <barral@math.lmu.de>
minlog (4.0.99-1) unstable; urgency=low
* Initial release

See Also

Package Description
minpack-dev_19961126+dfsg1-1_amd64.deb nonlinear equations and nonlinear least squares static library
mipe_1.1-3_all.deb Tools to store PCR-derived data
mira-assembler_3.4.0.1-1_amd64.deb Whole Genome Shotgun and EST Sequence Assembler
mira-doc_3.4.0.1-1_all.deb documentation for the mira assembler
mira-examples_3.4.0.1-1_all.deb files to experiment with the mira assembler
mirage_0.9.5.1-1.1_amd64.deb fast and simple GTK+ image viewer
miredo-server_1.2.3-1ubuntu1_amd64.deb Teredo IPv6 tunneling server
miredo_1.2.3-1ubuntu1_amd64.deb Teredo IPv6 tunneling through NATs
mirmon_2.4-2_all.deb monitor the state of mirrors
miro-data_4.0.4-1_all.deb GTK+ based RSS video aggregator data files
miro_4.0.4-1_amd64.deb GTK+ based RSS video aggregator
mirror_2.9-59_all.deb keeps FTP archives up-to-date
mirrorkit_0.1.1-0ubuntu4_all.deb Python frontend to debmirror
mirrormagic-data_2.0.2.0deb1-9_all.deb Data files for mirrormagic
mirrormagic_2.0.2.0deb1-9_amd64.deb Shoot around obstacles to collect energy using your beam
Advertisement
Advertisement