This is going to be the homepage of a collection of software and proofs to support first-order theorem proving based on condensed detachment with proofs represented by D-terms and related methods.
The toolkit is currently under development. Material to reproduce the experiments described in
Christoph Wernhard and Wolfgang Bibel
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
In CADE-28, 2021, to appear
is archived at: