Commits · 74fce621fa35af3ee827184de721d7d64c1abfcc · LARA / lisa · GitLab

Snippets Groups Projects

Oct 03, 2022
- lisa-utils depend on scallion and silex for parsing · 74fce621
  Katja Goltsova authored 2 years ago
  
  74fce621
- Format build.sbt · 04aad4c8
  Katja Goltsova authored 2 years ago
  
  04aad4c8
- Introduce True and False constants, expressed as empty 'and' and empty 'or' respectively · 84edc289
  Katja Goltsova authored 2 years ago
  
  84edc289
Sep 29, 2022
- Merge pull request #45 from cache-nez/require-arity · 967f9ead
  SimonGuilloud authored 2 years ago
  Unverified
  
  967f9ead
- Merge branch 'main' into require-arity · e0a7260e
  SimonGuilloud authored 2 years ago
  
  Unverified
  
  e0a7260e
- Merge pull request #43 from sankalpgambhir/main · 6e3fd810
  SimonGuilloud authored 2 years ago
  Unverified
  
  6e3fd810
Sep 26, 2022
- Merge branch 'main' into main · ddf000f9
  Viktor Kunčak authored 2 years ago
  
  Unverified
  
  ddf000f9
Sep 25, 2022
- Move all Peano-related files into their own package · 5f70f712
  Katja Goltsova authored 2 years ago
  
  5f70f712
- Run scalafix on Peano · 1b3106f4
  Katja Goltsova authored 2 years ago
  
  1b3106f4
- Prove in Peano arithmetic that x+y=y+x · ebe05d5a
  Katja Goltsova authored 2 years ago
  
  ebe05d5a
- Generalize instantiateForallAxiom to instantiateForallImport · befd7976
  Katja Goltsova authored 2 years ago
  
  befd7976
- Factor out Peano induction application · 73a298ee
  Katja Goltsova authored 2 years ago
  
  73a298ee
- Use instantiateForallAxiom in the proof of x+0=0+x to clean up the left hand side of the proof · 152289c4
  Katja Goltsova authored 2 years ago
  
  152289c4
- Prove in Peano that x+Sy = Sx+y · 6e355f4d
  Katja Goltsova authored 2 years ago
  
  6e355f4d
- Prove in Peano arithmetics that x + 0 = 0 + x · 96085809
  Katja Goltsova authored 2 years ago
  
  96085809
- Introduce PeanoArithmetics, PeanoArithmeticsLibrary, Peano · 453f3674
  Katja Goltsova authored 2 years ago
  453f3674
- Create a running theory with Peano axioms · db5131ab
  Ekaterina Goltsova authored 2 years ago
  
  db5131ab
- added subset definition axiom · b5b141eb
  Sankalp Gambhir authored 2 years ago
  
  b5b141eb
Sep 19, 2022
- Require that PredicateFormula's and ConnectorFormula's args correspond to the label's arity · 4be9a1aa
  Katja Goltsova authored 2 years ago
  4be9a1aa
Sep 08, 2022
- Merge pull request #44 from cache-nez/broken-link · d0a96d1a
  SimonGuilloud authored 2 years ago
  Unverified
  
  d0a96d1a
Sep 05, 2022
- Fix a broken link to the reference manual · 9855b826
  Katja Goltsova authored 2 years ago
  
  9855b826
Sep 02, 2022
- Grammatical updates for part 2 · 66ea4a60
  Sankalp Gambhir authored 2 years ago
  
  Unverified
  
  66ea4a60
- Grammatical edits for introduction and part 1 · 05ea36da
  Sankalp Gambhir authored 2 years ago
  Unverified
  
  05ea36da
Aug 28, 2022
- Removed old manual. · 51d9edb1
  SimonGuilloud authored 2 years ago
  
  51d9edb1
- Reworked LISA Reference Manual. · 9f55898f
  SimonGuilloud authored 2 years ago
  
  9f55898f
Aug 05, 2022
- Add utils to follow the path to an incorrect proof step and to create an error... · 6172b840
  Katja Goltsova authored 2 years ago
  6172b840
- Add a test to make sure that the path to the first invalid proof step is reported correctly · e13332be
  Katja Goltsova authored 2 years ago
  
  e13332be
- In CI, run tests before checking style · 00ca4fbf
  Katja Goltsova authored 2 years ago
  
  00ca4fbf
Aug 02, 2022
- In ProofCheckerSuite#checkProof, fail if the proof is not valid · 7335d23c
  Katja Goltsova authored 2 years ago
  
  7335d23c
Jul 19, 2022
- Add a test theory to facilitate writing proof assistant tests · cf545d8f
  Katja Goltsova authored 2 years ago
  
  cf545d8f
- Changed printer test. · 620f7056
  SimonGuilloud authored 2 years ago
  620f7056
- ran scalafixAll · 4c6aa9a9
  SimonGuilloud authored 2 years ago
  
  4c6aa9a9
- Ran scalafmt · e8aa5ca8
  SimonGuilloud authored 2 years ago
  
  e8aa5ca8
- Updated tests and examples. · be90afcf
  SimonGuilloud authored 2 years ago
  
  be90afcf
- Corrected eroneous proof. Created VariableFormulaLabel to replace arity-0 predicate schemas. · b401364e
  SimonGuilloud authored 2 years ago
  b401364e
- Changed the whole project to remove 0-arity schematic variables and replace... · eab5e80a
  SimonGuilloud authored 2 years ago
  eab5e80a
Jun 24, 2022
- Moved project lisa to root · 034c70fa
  SimonGuilloud authored 2 years ago
  034c70fa
Jun 23, 2022
- Move src/ to lisa/src/ for consistency · 8f293007
  Florian Cassayre authored 2 years ago
  
  8f293007
- Re-enable scalafix/scalafmt, re-format everything · fbc8c0df
  Florian Cassayre authored 2 years ago
  
  fbc8c0df
- Complete re-organization into separate modules · 9f9f285a
  Florian Cassayre authored 2 years ago
  
  9f9f285a