Home

Downloads

Examples

Documents

Psyche

the Proof-Search factorY for Collaborative HEuristics

Documentation

[GL13] S. Graham-Lengrand. Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture. In D. Galmiche and D. Larchey-Wendling, editors, Proc. of the 22nd Intern. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), volume 8123 of LNCS, pages 149-156. Springer-Verlag, September 2013.
[pdf]
[FGLM13] M. Farooque, S. Graham-Lengrand, and A. Mahboubi. A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. In A. Momigliano, B. Pientka, and R. Pollack, editors, Proc. of the 2013 Intern. Work. on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2013). ACM Press, September 2013.
[pdf]