sneeuwballen/zipperposition

Issues

• Assert error in Literals.ml when calling E with trivial goal

  #99 opened 8 months ago by nartannt
  3

• Linux build fail

  #95 opened a year ago by apease
  7

• Unquoted predicate names in TPTP output

  #93 opened 2 years ago by TpmKranz
  2

• parallel make fails

  #92 opened 2 years ago by medovina
  6

• infix syntax doesn't work

  #90 opened 2 years ago by medovina
  2

• Support for answer tuples

  #89 opened 3 years ago by logicReasoner
  4

• Can't parse TIP v0.3

  #88 opened 3 years ago by TpmKranz
  4

• Using Zipperposition with THF syntax

  #82 opened 4 years ago by mcoulont
  3

• Assertion failed in superposition.ml

  #81 opened 4 years ago by mcoulont
  3

• Assertion failed

  #79 opened 4 years ago by mcoulont
  7

• exception in proof checking

  #78 opened 4 years ago by c-cube
  0

• type error in induction

  #77 opened 5 years ago by c-cube
  0

• give up instead of erroring on `real` arith problems

  #76 opened 5 years ago by c-cube
  0

• sometimes kbo is really bad

  #75 opened 5 years ago by c-cube
  0

• investigate bad behavior of int-semantic-tauto

  #74 opened 5 years ago by c-cube
  0

• parse error on Problems/SYO/SYO042^2.p

  #72 opened 5 years ago by c-cube
  0

• type inference error on Problems/SEU/SEU916^5.p

  #71 opened 5 years ago by c-cube
  0

• type inference for CSR

  #70 opened 5 years ago by c-cube
  0

• OCamlFormat

  #51 opened 5 years ago by abentkamp
  1

• Use FlexState for all cli options

  #46 opened 5 years ago by abentkamp
  0

• portfolio inside zipperposition

  #50 opened 5 years ago by c-cube
  0

• Proof checking: Issue with lambda-expressions and sidekick

  #67 opened 5 years ago by abentkamp
  1

• tracking: proof checking

  #58 opened 5 years ago by c-cube
  0

• Clause.proof_depth counts ESA-steps as 0

  #66 opened 5 years ago by abentkamp
  6

• problem with weak-head normal form

  #65 opened 5 years ago by petarvukmirovic
  1

• proof checking for avatar

  #64 opened 5 years ago by abentkamp
  2

• use DB indices in term rewriting/demod

  #63 opened 5 years ago by c-cube
  0

• Otter loop?

  #62 opened 5 years ago by c-cube
  0

• tracking: rewriting

  #61 opened 5 years ago by c-cube
  0

• tracking: datatypes

  #60 opened 5 years ago by c-cube
  0

• tracking: induction

  #59 opened 5 years ago by c-cube
  0

• investigate GEG problems

  #57 opened 5 years ago by c-cube
  0

• proof checking for arith ℤ

  #56 opened 5 years ago by c-cube
  0

• proof checking for arith ℚ

  #55 opened 5 years ago by c-cube
  0

• sat grounding

  #49 opened 5 years ago by petarvukmirovic
  1

• HOT ISSUE: ST.AppBuiltin

  #54 opened 5 years ago by petarvukmirovic
  9

• fast proof checker

  #53 opened 5 years ago by c-cube
  0

• proof checking for full HO

  #52 opened 5 years ago by c-cube
  0

• investigate docker+alpine for starexec build

  #39 opened 5 years ago by c-cube
  1

• Higher-order reasoning is incomplete

  #25 opened 7 years ago by rafoo
  6

• CCOrd.compare fixes

  #47 opened 5 years ago by petarvukmirovic
  2

• Caching of ordering status

  #42 opened 5 years ago by petarvukmirovic
  4

• perfect discrimination tree fixes (weight + trace)

  #48 opened 5 years ago by petarvukmirovic
  2

• CNF common formulas renaming

  #41 opened 5 years ago by petarvukmirovic
  2

• Rename `Unif.FO`, `Subst.FO`, etc

  #45 opened 5 years ago by abentkamp
  1

• Orphan deletion

  #44 opened 5 years ago by petarvukmirovic
  0

• Reported status

  #43 opened 5 years ago by petarvukmirovic
  0

• How to access Logtk

  #36 opened 6 years ago by darrenldl
  6

• enforce def-as-rewrite

  #26 opened 7 years ago by c-cube
  0

• exception raised in signal: Error: invalid_argument: as_const_exn

  #24 opened 7 years ago by rafoo
  0