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

Stéphane Graham-Lengrand

Published in: TABLEAUX (2013)

Keyphrases

sequent calculus
linear logic
cut elimination
search engine
inference rules
natural deduction
modal logic
proof search
web search
theorem prover
web search engines
linear time temporal logic
fixed point
web pages
logical framework
wide class
artificial intelligence
temporal logic