Finite Quantification in Hierarchic Theorem Proving

DOI10.1007/978-3-319-08587-6_11zbMATH Open1423.68407OpenAlexW1489937864MaRDI QIDQ3192187FDOQ3192187

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

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (10)

• Coming to terms with quantified reasoning
• On the generation of quantified lemmas
• Hierarchic superposition revisited
• A superposition calculus for abductive reasoning
• Automated Inference of Finite Unsatisfiability
• Automated inference of finite unsatisfiability
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constraint solving for finite model finding in SMT solvers
• Combining induction and saturation-based theorem proving

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)