Home
Projects
Resources
Alternatives
Blog
Sign In
Gapt Versions
Save
GAPT: General Architecture for Proof Theory
Overview
Versions
Reviews
Resources
v2.0
1 year ago
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
v2.1
1 year ago
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)
v2.2
1 year ago
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
v2.3
1 year ago
The minimum required Java version is now Java 8
String interpolators for sequents
:-
operator to construct sequents
loadExpansionProof
provides 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
v2.4
1 year ago
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
v2.5
1 year ago
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
v2.6
1 year ago
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
v2.7
1 year ago
Conversion from LK to natural deduction
Induction elimination
Grammar generation for Π₂-cut introduction
v2.8
1 year ago
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
v2.9
1 year ago
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{...}
or
tactic.verbose
to 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
« Previous
Next »
Home
Projects
Resources
Alternatives
Blog
Sign In
Sign In to OSA
I agree with
Terms of Service
and
Privacy Policy
Sign In with Github