Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture

DOI10.1007/978-3-642-40537-2_14zbMath1401.68277OpenAlexW2208061263MaRDI QIDQ2851941

Stéphane Graham-Lengrand

Publication date: 4 October 2013

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-00906789/file/Psyche.pdf

Mathematics Subject Classification ID

Related Items (5)

Improving complex SMT strategies with learning ⋮ Axiomatic Constraint Systems for Proof Search Modulo Theories ⋮ Stoic Sequent Logic and Proof Theory ⋮ Scalable fine-grained proofs for formula processing ⋮ Psyche

Uses Software

• Coq
• Isabelle
• LCF

This page was built for publication: Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture