Automating Free Logic in Isabelle/HOL
From MaRDI portal
Publication:2819197
DOI10.1007/978-3-319-42432-3_6zbMath1434.68638MaRDI QIDQ2819197
Christoph Benzmüller, Dana S. Scott
Publication date: 28 September 2016
Published in: Mathematical Software – ICMS 2016 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-42432-3_6
free logic; model finding; interactive and automated theorem proving; application to category theory
03B60: Other nonclassical logic
03B35: Mechanization of proofs and logical operations
03B16: Higher-order logic
18A15: Foundations, relations to logic and deductive systems
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Uses Software
