Evidence algorithm and inference search in first-order logics

DOI10.1007/s10817-015-9346-0zbMath1356.03055MaRDI QIDQ286802

F. Blanchet-Sadri, M. Dambrine

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-015-9346-0

zbMATH Keywords

modal logic; first-order logic; sequent calculus; Maslov's inverse method; intuitionistic logic; automated theorem proving; classical logic; clash-resolution method; evidence algorithm; inference search

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03F07: Structure of proofs

Uses Software

• Mizar
• SAD
• ForTheL