Deciding the Inductive Validity of ∀ ∃ * Queries

DOI10.1007/978-3-642-04027-6_25zbMath1257.03031OpenAlexW1934037091MaRDI QIDQ3644758

Christoph Weidenbach, Matthias Horbach

Publication date: 12 November 2009

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04027-6_25

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25)

Related Items (5)

Symbol elimination and applications to parametric entailment problems ⋮ System Description: SPASS-FD ⋮ Combining induction and saturation-based theorem proving ⋮ On invariant synthesis for parametric systems ⋮ Deciding the Inductive Validity of ∀ ∃ * Queries

Cites Work

• Automating inductionless induction using test sets
• Equational problems and disunification
• A method for simultaneous search for refutations and models by equational constraint solving
• Automated theorem proving by test set induction
• Model building with ordered resolution: Extracting models from saturated clause sets
• Induction = I-axiomatization + first-order consistency.
• Automata-driven automated induction
• Superposition for Fixed Domains
• Deciding the Inductive Validity of ∀ ∃ * Queries
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Inductive Decidability Using Implicit Induction
• Logic for Programming, Artificial Intelligence, and Reasoning
• Unnamed Item
• Unnamed Item

This page was built for publication: Deciding the Inductive Validity of ∀ ∃ * Queries