Cooperation of background reasoners in theory reasoning by residue sharing

DOI10.1023/A:1022587501759zbMath1019.03004OpenAlexW2175599263MaRDI QIDQ1810855

Cesare Tinelli

Publication date: 9 June 2003

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

Full work available at URL: https://doi.org/10.1023/a:1022587501759

zbMATH Keywords

theory reasoningmultiple background reasoners

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (11)

Combining nonstably infinite theories ⋮ Modular proof systems for partial functions with Evans equality ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Quantifier Elimination and Provers Integration ⋮ Combining Non-Stably Infinite Theories ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ Ground Interpolation for the Theory of Equality ⋮ Politeness and combination methods for theories with bridging functions ⋮ Differential dynamic logic for hybrid systems ⋮ Polite combination of algebraic datatypes ⋮ Combining sets with cardinals

This page was built for publication: Cooperation of background reasoners in theory reasoning by residue sharing