- Fix developer information
- Publish to Maven Central
- CLI is the entry point of the JAR file
- Fixes some occurrences of the Scala version number
- Updates to the 2.15 release notes
- DLS algorithm for formula equations
- Spin: saturation-based induction prover
- Update to Scala 2.13
- Refactoring of TIP tools, HOL to FOL translation and iProver interface
- Bug fixes
- Slakje: performance improvements
- Escargot: discrimination trees and feature vector indices.
- New term-based expansion tree implementation.
- Support for E 2.2.
- Slakje: automated theorem prover for first-order intuitionistic logic.
- JSON export and import for proofs and expressions
- Kolmogorov and Friedman translations
- SMTInterpol interface
- Support for Vampire 4.2.2
- JSON Serialization for expressions, LK Proofs, ND Proofs
- Improvements to the TIP Parser
- TPTP/TSTP Statistics
- New proof schemata
- Deskolemization of proofs with equational reasoning
- Root package was renamed from
at.logic.gaptto justgapt - Modified realizability
- New reductive cut-elimination implementation for LK
- Emoji support in formulas
- Implication is now → (instead of ⊃)
- LKt: proof terms for high performance cut normalization
- IEscargot prototype: an effective prover for first-order intuitionist logic
- User-defined operators in Babel (the formula parser)
- Simplifier tactic
- Formalization of the Fundamental Theorem of Arithmetic
- Hierarchical logging levels
- Many bugfixes for parametric polymorphism
- Support for the current (yet unreleased) TIP format
- Rewrite of the tree grammar-based induction prover
- Atomic expansion for expansion proofs
- Restructured user manual
- The Scala operator for function types is now
->:instead of-> - Logback logging library was removed, use
verbose{...}ortactic.verboseto enable logging - Schematic structs and characteristic formulas for CERES
- Support for iProver 2.7
- Induction support for ExpansionProofToLK, LKToExpansionProof
- Constants now have an explicit list of type parameters
- Support for EProver 2.0
- Support for Vampire 4.2
- Experimental support for iProver (requires current development version)
- MutableContext now keeps track of automatically generated Skolem functions
- Cut-elimination no longer regularizes
- deskolemizeET now supports inner Skolemization
- Conversion from LK to natural deduction
- Induction elimination
- Grammar generation for Π₂-cut introduction
- Natural deduction
- Free monad for the SMT solver interface
- Portfolio mode in new viper command-line interface
- Skolemization with free variables support in ResolutionProver.getLKProof
- Primitive recursive definitions
- Proof schemata
- ACNF support in reductive cut-elimination
- Support veriT stable2016
- CERES version that directly produces expansion proofs
- Deskolemization
- First prototype of Pi2 cut-introduction
- Better error messages in Babel, the formula parser
- Update to Scala 2.12
- LKsk and Ral are replaced by the standard calculi, CERESω is now just CERES.
- Analytic induction prover
- Tons of proofs for problems from TIP
- Refactored Context data structure to enable future support for recursors
- The minimum required Java version is now Java 8
- String interpolators for sequents
:-operator to construct sequentsloadExpansionProofprovides convenient access to TSTP proof import- Refactored prooftool supports n-ary inferences now
- Conversion of unit-equational resolution proofs to unary LK proofs
- Special class for polarities instead of Booleans
- Support for Vampire 4.1
- Support for SPASS 3.9
- Context now support polymorphic declarations (for equality, ...)
- Many-sorted grammars
- Sound definition rules for LK
- New resolution calculus with Avatar splitting
- Vampire proof import with splitting
- More reliable leanCoP interface
- Metis interface
- TPTP problem parser
- Removal of obsolete or unmaintained code:
- Schemata
- Old LK implementation
- Old LKsk implementation
- Old LLK parser
- Old Delta-Table implemenetation
- XML parser
- Skolem inferences for LK
- Sequent is now a case class
- Subproofs can be hidden in prooftool now
- Escargot, a simple built-in superposition prover
- New expansion tree implementation, now with cuts!
- Type classes for types that are closed under substitution
- gaptic, LK proof input using tactics
- Most of the included proofs are converted to gaptic
- Faster delta-table algorithm
- Complete input/output format Babel with string interpolators
- Context class that stores data types, constants, definitions, etc.
- SPASS interface supporting splitting inferences
- Skolem symbol validation
- Many-sorted to first-order reduction
- DRUP proof import from SAT solvers (Sat4j, PicoSAT, and Glucose)
- Refactoring of (most) calculi (LK, resolution mainly)
- Replay-based proof import for TPTP proofs, including a Vampire and E interface
- New cut-intro code that doesn't need interpolation
- sbt console
- Cleaned up prooftool now supports multiple open windows at once
- Brand new CERES implementation
- Tons of bug fixes