Code

Skolemization#876

Code

Open

Taissirbw wants to merge 26 commits intoDeducteam:masterDeducteam/lambdapi:masterfrom Taissirbw:masterTaissirbw/lambdapi:masterCopy head branch name to clipboard

+397-158

Commits

Commits on May 29, 2022

• Tactique de skolémisation

  

  taissir.marce

  committed
  389c597

  Copy full SHA for 389c597

Commits on May 30, 2022

• Définition de P_tac_skolem dans handle.ml

  

  taissir.marce

  committed
  32ac1ca

  Copy full SHA for 32ac1ca

Commits on Jun 2, 2022

• Merge branch 'master' of https://gitlab.dsi.universite-paris-saclay.fr/taissir.marce/skolemisation

  

  taissir.marce

  committed
  717e229

  Copy full SHA for 717e229

Commits on Jun 7, 2022

• Correction axiome dans la tactique skolemisation

  

  taissir.marce

  committed
  0c03448

  Copy full SHA for 0c03448

• suppression tests/skolem.ml

  

  taissir.marce

  committed
  c645016

  Copy full SHA for c645016

Commits on Jul 4, 2022

• nnf + prenexe

  

  taissir.marce

  committed
  0f90c9f

  Copy full SHA for 0f90c9f

Commits on Jul 6, 2022

• Tactique de skolemisation : Mise en NNF et forme prenexe avant l'elimination des existentiels

  

  taissir.marce

  committed
  bd69824

  Copy full SHA for bd69824

• Print pour debug en commentaire

  Taissirbw

  committed
  dbdb3a0

  Copy full SHA for dbdb3a0

• Merge branch 'Deducteam:master' into master

  Taissirbw

  authored
  f5e1a78

  Copy full SHA for f5e1a78

Commits on Jul 21, 2022

• Merge branch 'master' into skolemAndFriends@v2

  

  gabrielhdt

  committed
  1dacef2

  Copy full SHA for 1dacef2

• Formatting with ocamlformat

  Show description for 9052a47
  

  gabrielhdt

  committed
  9052a47

  Copy full SHA for 9052a47

• Expose prenex, nnf, tests

  

  gabrielhdt

  committed
  ac1183a

  Copy full SHA for ac1183a

• Merge pull request #2 from gabrielhdt/skolemAndFriends@v2

  Show description for 9824139
  Taissirbw

  authored
  9824139

  Copy full SHA for 9824139

Commits on Dec 28, 2022

• Merge remote-tracking branch 'lp/master' into skolem

  fblanqui

  committed
  6e6ca92

  Copy full SHA for 6e6ca92

• fix compil and sanity check

  fblanqui

  committed
  a87af92

  Copy full SHA for a87af92

• factorize fol config with why3_tactic

  fblanqui

  committed
  feb5f9c

  Copy full SHA for feb5f9c

• renamings

  fblanqui

  committed
  9e4c0e6

  Copy full SHA for 9e4c0e6

Commits on Dec 29, 2022

• tactics do not need to generate new sig_state as axioms do not need to be added in scope

  fblanqui

  committed
  ac42164

  Copy full SHA for ac42164

• why3 tactic: let tac_admit generate the axiom

  fblanqui

  committed
  14e775f

  Copy full SHA for 14e775f

• detail

  fblanqui

  committed
  cecef15

  Copy full SHA for cecef15

• Merge remote-tracking branch 'lp/master' into skolem

  fblanqui

  committed
  9d70df4

  Copy full SHA for 9d70df4

Commits on Dec 30, 2022

• Merge remote-tracking branch 'lp/master' into skolem

  fblanqui

  committed
  d4bd83a

  Copy full SHA for d4bd83a

Commits on Dec 31, 2022

• Merge remote-tracking branch 'lp/master' into skolem

  fblanqui

  committed
  f6b024c

  Copy full SHA for f6b024c

Commits on Jan 2, 2023

• Merge remote-tracking branch 'lp/master' into skolem

  fblanqui

  committed
  da2d59c

  Copy full SHA for da2d59c

Commits on Jan 3, 2023

• update bnf grammar

  fblanqui

  committed
  f4a3ec7

  Copy full SHA for f4a3ec7

Commits on Jan 11, 2023

• Merge remote-tracking branch 'lp/master' into skolem

  fblanqui

  committed
  abf7e6b

  Copy full SHA for abf7e6b