Theory Instantiation

DOI10.1007/11916277_34zbMath1165.03315OpenAlexW2911619792MaRDI QIDQ5387915

Konstantin Korovin, Harald Ganzinger

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)

Related Items (10)

Semantically-guided goal-sensitive reasoning: model representation ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Satisfiability Modulo Theories ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Making theory reasoning simpler ⋮ 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