Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Oct 13, 2017

• Redo the axiomatic development of geometric algebra. The question of

  Show description for 51ba0bb
  

  Jason Hickey

  committed
  51ba0bb

  Copy full SHA for 51ba0bb

• Initial WF for vector spaces.

  

  Jason Hickey

  committed
  0030e36

  Copy full SHA for 0030e36

Commits on Oct 12, 2017

• Update supinf to use Refiner.Refiner.TermMan

  

  Jason Hickey

  committed
  4d94cb2

  Copy full SHA for 4d94cb2

• Refine the Refiner.Refiner include. It caused RefineError to get a NULL

  Show description for 74d91b5
  

  Jason Hickey

  committed
  74d91b5

  Copy full SHA for 74d91b5

• Fix some syntax errors :P

  

  Jason Hickey

  committed
  616bdec

  Copy full SHA for 616bdec

Commits on Oct 5, 2017

• Starting work in vector spaces.

  

  Jason Hickey

  committed
  dc920a4

  Copy full SHA for dc920a4

Commits on Sep 25, 2017

• First working compile with OCaml 4.05.

  

  Jason Hickey

  committed
  cc30327

  Copy full SHA for cc30327

Commits on Sep 24, 2017

• Refiner compiles for OCaml 4.05, but the theories are not yet working.

  

  Jason Hickey

  committed
  9bcaffb

  Copy full SHA for 9bcaffb

Commits on Sep 23, 2017

• More progress fixng the filter for OCaml 4.05.

  

  Jason Hickey

  committed
  a09c164

  Copy full SHA for a09c164

Commits on Sep 20, 2017

• Add missing expressions. filter_ocaml.ml now compiles.

  

  Jason Hickey

  committed
  58d0260

  Copy full SHA for 58d0260

• Added most missing expressions in filter_ocaml.ml. Still expr/patt to

  Show description for efb1926
  

  Jason Hickey

  committed
  efb1926

  Copy full SHA for efb1926

Commits on Sep 19, 2017

• Initial progress toward support OCaml 4.05.

  Show description for d34a0b0
  

  Jason Hickey

  committed
  d34a0b0

  Copy full SHA for d34a0b0

Commits on Sep 13, 2017

• Initial progress for porting to 4.02.3.

  

  Jason Hickey

  committed
  2896475

  Copy full SHA for 2896475

Commits on Dec 18, 2008

• fixed a couple of minor bugs in some Gilbert-style proof steps

  

  yegor

  committed
  70c3b7a

  Copy full SHA for 70c3b7a

Commits on Aug 14, 2008

• Realization for Wise Men and some formulations of Muddy Children (those that we tried) seems to work.

  Show description for fcae8b1
  

  yegor

  committed
  fcae8b1

  Copy full SHA for fcae8b1

Commits on Jul 16, 2008

• added NegRight.

  Show description for ddd2fdb
  

  yegor

  committed
  ddd2fdb

  Copy full SHA for ddd2fdb

• OrRight added

  

  yegor

  committed
  0299bc0

  Copy full SHA for 0299bc0

• added OrLeft

  

  yegor

  committed
  bf928fb

  Copy full SHA for bf928fb

• forgot to add these files a couple of days ago

  

  yegor

  committed
  e8b0d37

  Copy full SHA for e8b0d37

• added AndLeft

  

  yegor

  committed
  fe14d06

  Copy full SHA for fe14d06

• Added AndRight rule and it exposed an error g2h code for BoxRight (lemma3 was implemented incorrectly and worked only for one hypothesis).

  Show description for ef09ebd
  

  yegor

  committed
  ef09ebd

  Copy full SHA for ef09ebd

Commits on Jul 15, 2008

• more progress towards multi-modal case

  

  yegor

  committed
  3ee4262

  Copy full SHA for 3ee4262

• Added Nec rule, in its generic (not restricted to axioms) form.

  Show description for 8120900
  

  yegor

  committed
  8120900

  Copy full SHA for 8120900

• eliminated explicit references to axiom indices and arithmetic over them (where necessitation was needed)

  

  yegor

  committed
  c38a71b

  Copy full SHA for c38a71b

Commits on Jul 13, 2008

• a tiny simplification

  

  yegor

  committed
  7646d74

  Copy full SHA for 7646d74

• added connection with JProver.

  Show description for ac3c877
  

  yegor

  committed
  ac3c877

  Copy full SHA for ac3c877

Commits on Jul 11, 2008

• Added some code that extracts and prints all formulas that were claimed tautologies (and left unproven) in the proof.

  Show description for 235fce7
  

  yegor

  committed
  235fce7

  Copy full SHA for 235fce7

Commits on Jul 10, 2008

• added phase1-2 substitution between families computation (assign) and realization per se (g2h)

  Show description for ecf3394
  

  yegor

  committed
  ecf3394

  Copy full SHA for ecf3394

• Changed the families handling code because merging of families was incorrectly implemented. It used to be amp from representatives to the whole family, but if you think even a bit, you'll realize t…

  Show description for 9a11069
  

  yegor

  committed
  9a11069

  Copy full SHA for 9a11069

Commits on Jul 9, 2008

• compiles, runs and even checks up for self-referencial example.

  Show description for 9177fc4
  

  yegor

  committed
  9177fc4

  Copy full SHA for 9177fc4

Commits on Jul 5, 2008

• all phases finished in first draft, it compiles but never executed yet

  Show description for fe3ccfb
  

  yegor

  committed
  fe3ccfb

  Copy full SHA for fe3ccfb

Commits on Jul 4, 2008

• first draft of phase 1 finished

  

  yegor

  committed
  8c6d42a

  Copy full SHA for 8c6d42a

Commits on Jul 3, 2008

• added box-to-right rule to phase 1

  Show description for 5d9bb94
  

  yegor

  committed
  5d9bb94

  Copy full SHA for 5d9bb94

Commits on Jul 2, 2008

• working on phases 1 and 2

  

  yegor

  committed
  d6bc9a6

  Copy full SHA for d6bc9a6

Commits on Jun 30, 2008

• third phase is roughly finished.

  Show description for 1c1dcce
  

  yegor

  committed
  1c1dcce

  Copy full SHA for 1c1dcce

Pagination

Previous

Next