Theory Instantiation

DOI10.1007/11916277_34MaRDI QIDQ5387915zbMATH OpenOpenAlexFDO

Authors Harald Ganzinger, Konstantin Korovin

Publication date 27 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11916277_34

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Instantiation schemes for nested theories
• Constructor theory
• Instantiation theory. On the foundations of automated deduction
• scientific article; zbMATH DE number 1552527
• On the formalization of theories
• Theories as types
• scientific article; zbMATH DE number 440122
• Theory of semi-instantiation in abstract argumentation
• Theory by process
• A note on existential instantiation

Cited in

(14)

• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Modular instantiation schemes
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Making theory reasoning simpler
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Semantically-guided goal-sensitive reasoning: model representation
• Adding decision procedures to SMT solvers using axioms with triggers
• Instantiation schemes for nested theories
• Satisfiability modulo theories
• An instantiation scheme for satisfiability modulo theories
• Harald Ganzinger's legacy: contributions to logics and programming
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Planning with effectively propositional logic
• Model Evolution with Equality Modulo Built-in Theories

This page was built for publication: Theory Instantiation

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