Analytic tableaux for higher-order logic with choice
From MaRDI portal
Publication:438561
DOI10.1007/s10817-011-9233-2zbMath1258.03019MaRDI QIDQ438561
Julian Backes, Chad Edward Brown
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9233-2
higher-order logic; axiom of choice; automated theorem proving; tableau calculus; Henkin models; higher-order automated theorem-prover \texttt{Satallax}; simple type theory with choice
03B35: Mechanization of proofs and logical operations
03E25: Axiom of choice and related propositions
Related Items
Uses Software