package phox

  1. Overview
  2. Docs
PhoX is an implementation of Higher Order Logic

Install

Dune Dependency

Authors

Maintainers

Sources

phox.tar.gz
sha256=32715a5f270431e88bbee589dd7f5cb2bd08f40ab941fa9863263f64dd0ab7d8
md5=75636a8bc92f5336acf5708747ad3872

Description

Its main charateritics are

  • Tactics such as intro or rewrite can be extended by arbitrary theorems
  • As these tactics are used by the auto tactics, this allows to program the auto tatics.
  • You can produce nice latex documents.
  • doc/library/examples/tutorials are available.
  • ...

Authors:

Published: 16 Oct 2017

README

README

The folder constains examples to learn how to use PhoX.

Each example uses a file with "holes" to fill named xxx_quest.phx, and
a complete file named xxx_cor.phx.

These examples cover some precise points:

- tautologie_quest.phx

  The goal of this example is two sided:
  - We progressively introduce the simplest commands of PhoX on simple
    formulas of prositional logic or predicate calculus.
  - These examples can also be used as an introduction in logic for students.

- sort_quest.phx
  
  Covers a relatively advanced use of the software using the new_intro, 
  new_elim and new_rewrite commands which allow to change the behavior and
  the proof tactics (intro, elim, left, trivial, ...)

- Exo de math (fichiers ideal_quest.phx,
               commutation_quest.phx, topo_quest.phx,
               analyse_quest.phx et group_quest.phx)

  Des exercices pour apprendre les math en utilisant PhoX (on apprend
  PhoX en même temps, mais le but réel est d'apprendre des maths !)
  
- Logique Minimale (fichier minlog_quest.phx )

  But similaire au précédent, mais le sujet s'adresse plus à un logicien
  de bon niveau. 

Dependencies (3)

  1. camlp4 build
  2. ocamlfind build
  3. ocaml >= "4.02.0" & < "4.06.0"

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.