Commits · 1471cb81cd25dab2cd80423097c2250ce8925679 · veriT / Alethe

Aug 07, 2024
- Add or_intro rule · 1471cb81
  Hans-Jörg authored 9 months ago
  
  1471cb81
- Rename negative_ to nonpositive_ · eaeb3951
  Hans-Jörg authored 11 months ago
  
  eaeb3951
- No division by 0 in rational constants · 0258cc6c
  Hans-Jörg authored 11 months ago
  
  0258cc6c
- Change la_generic to use the new number formats · a686dd90
  Hans-Jörg authored 11 months ago
  
  a686dd90
- Fix potential typo? · beb818fb
  Lachnitt authored 9 months ago
  
  beb818fb
Jul 17, 2024
- Add index to and_pos, or_neg, and, not_or · df8503ac
  Hans-Jörg authored 9 months ago
  
  df8503ac
Jul 15, 2024
- Add eq_symmetric to rule classification tables · f359b2bc
  Hans-Jörg authored 9 months ago
  
  f359b2bc
Jun 11, 2024
- adding new rule · 8d4b1483
  Haniel Barbosa authored 10 months ago
  
  8d4b1483
Jun 03, 2024
- Change args of forall_inst to not give explicit bindings · 7015dbd1
  Hans-Jörg authored 11 months ago
  
  7015dbd1
- Add symm and not_symm rules. · 1f367fc9
  Hans-Jörg authored 11 months ago
  
  1f367fc9
- Add list of rules that are only used by cvc5 · f8dcee14
  Hans-Jörg authored 11 months ago
  
  f8dcee14
May 28, 2024
- Apply 1 suggestion(s) to 1 file(s) · a07a3f6d
  Haniel Barbosa authored 11 months ago and Lachnitt committed 11 months ago
  
  Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
  a07a3f6d
- Delete accidental copy · fbea37e0
  Lachnitt authored 11 months ago
  
  fbea37e0
- Apply 3 suggestion(s) to 1 file(s) · 8535f765
  Hans-Jörg authored 11 months ago and Lachnitt committed 11 months ago
  
  Co-authored-by: Hans-Jörg <commits@schurr.at>
  8535f765
May 24, 2024
- Add draft for la mult rules · b7c1ff6b
  Lachnitt authored 11 months ago
  
  b7c1ff6b
May 08, 2024
- Clarifiy that bind can work on ∃ and ∀ · 17f0b594
  Hans-Jörg authored 1 year ago
  
  Addresses #37
  17f0b594
- Fix typo in forall_inst · 4dedd4ec
  Hans-Jörg authored 1 year ago
  
  Adresses #35
  4dedd4ec
- Fix context description in subproof closing rules. · f8a1cdc8
  Hans-Jörg authored 1 year ago
  
  Addresses #36
  f8a1cdc8
May 06, 2024

Set hypertexnames to false for hyperref package to fix references · 15b1cffb

Hans-Jörg authored 1 year ago

This follows the advice given here:
https://latex.org/forum/viewtopic.php?t=32205
The option changes how destination names are defined.

Also fixes two other small typos related to references.

Should address:
#39

15b1cffb

Fix example for onepoint proof rule · 74c14093
Hans-Jörg authored 1 year ago
```
Addresses #40
```
74c14093

Mar 19, 2024
- Add bitvector rules list · c234c12a
  Hans-Jörg authored 1 year ago
  
  c234c12a
- Bitblasting: adapt notation · f081142f
  Hans-Jörg authored 1 year ago
  
  f081142f
- adding rules for bvult and bvadd · 9461e5f9
  Haniel Barbosa authored 1 year ago and Hans-Jörg committed 1 year ago
  
  9461e5f9
- fixes · 6b8582ba
  Haniel Barbosa authored 1 year ago and Hans-Jörg committed 1 year ago
  
  6b8582ba
- defining bitblasting rules · 09f3e612
  Haniel Barbosa authored 1 year ago and Hans-Jörg committed 1 year ago
  
  09f3e612
Jan 05, 2024
- Fix typos in la_tautology · dedf61eb
  Hans-Jörg authored 1 year ago
  
  dedf61eb
Jul 20, 2023
- fix `false` rule (as Hanna reported) · 209e2c6c
  Haniel Barbosa authored 1 year ago
  
  209e2c6c
Feb 10, 2023
- More edits · bab61d95
  Hans-Jörg Schurr authored 2 years ago
  
  - adress normalizing of terms with context push (and other typos) - Remark on missing Gamma
  bab61d95
- Clarify role of alpha-equivalence when checking the context · 2c28f6f3
  Hans-Jörg Schurr authored 2 years ago
  
  2c28f6f3
- Add language about capture-avoiding · 99d28a75
  Hans-Jörg Schurr authored 2 years ago
  
  99d28a75
- Remove trailing whitespaces · 9dab69e5
  Hans-Jörg Schurr authored 2 years ago
  
  9dab69e5
- Apply textual and typographic improvements · 9753d4b7
  Hans-Jörg Schurr authored 2 years ago
  
  - replace semantic by semantics - apply some review suggestions
  9753d4b7
- Remove redundant simplification from `implies_simplify` · 5f5939fe
  Hans-Jörg authored 2 years ago
  
  The simplification `(P -> Q) -> Q => P or Q` is already covered by `bool_simplify`.
  5f5939fe
- Overwrite "rule_list.tex" with new rules list · a8abc836
  Hans-Jörg authored 2 years ago
  
  a8abc836
Aug 23, 2022
- More tweaks to rule list · 3347b1c4
  Hans-Jörg authored 2 years ago
  
  3347b1c4
Aug 21, 2022
- More small tweaks in the rule list · ed3ba9f6
  Hans-Jörg authored 2 years ago
  
  ed3ba9f6
Aug 19, 2022
- la_generic: tiny typographic tweaks · 59fa92a9
  Hans-Jörg authored 2 years ago
  
  59fa92a9
Aug 18, 2022
- Fix typos · b075a3bc
  Hans-Jörg authored 2 years ago
  
  b075a3bc
- Fix typo · bd97b351
  Hans-Jörg authored 2 years ago
  
  bd97b351
Jul 02, 2022

Add formal semantic of Alethe · 70003228

Hans-Jörg authored 2 years ago

- Define what a valid Alethe proof is formally
- Show that a valid Alethe proof is sound
- TODO: nicer handling of let

70003228