Deciding the Inductive Validity of ∀ ∃ * Queries

DOI10.1007/978-3-642-04027-6_25zbMath1257.03031MaRDI 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

03B25: Decidability of theories and sets of sentences

Related Items

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

• Unnamed Item
• Unnamed Item
• 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