Finite Quantification in Hierarchic Theorem Proving

DOI10.1007/978-3-319-08587-6_11MaRDI QIDQ3192187zbMATHOpenAlexFDO

Authors Peter Baumgartner, Joshua Bax, Uwe Waldmann

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08587-6_11

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Higher-order quantification and proof search
• Finite quantifier hierarchies in relational algebras
• Towards a proof theory for Henkin quantifiers
• scientific article; zbMATH DE number 1163938
• The hierarchy theorem for generalized quantifiers
• scientific article; zbMATH DE number 1300967
• scientific article; zbMATH DE number 7668091
• Definability hierarchies of generalized quantifiers
• Provability logics with quantifiers on proofs
• scientific article; zbMATH DE number 1008505

Cited in

(10)

• Hierarchic superposition revisited
• scientific article; zbMATH DE number 1951638 (Why is no real title available?)
• Combining induction and saturation-based theorem proving
• scientific article; zbMATH DE number 4043224 (Why is no real title available?)
• Automated inference of finite unsatisfiability
• Coming to terms with quantified reasoning
• On the generation of quantified lemmas
• Automated Inference of Finite Unsatisfiability
• A superposition calculus for abductive reasoning
• Constraint solving for finite model finding in SMT solvers

This page was built for publication: Finite Quantification in Hierarchic Theorem Proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192187)