Quantifier-Free Equational Logic and Prime Implicate Generation

DOI10.1007/978-3-319-21401-6_21zbMath1465.68280OpenAlexW1417197267MaRDI QIDQ3454103

Mnacho Echenim, Sophie Tourret, Nicolas Peltier

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_21

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Logical reduction of metarules

Uses Software

• SOLAR
• SMT-LIB
• TPTP
• E Theorem Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Equality and abductive residua for Horn clauses
• An incremental method for generating prime implicants/implicates
• Theory decision by decomposition
• Implication of clauses is undecidable
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• System Description: E 1.8
• A Rewriting Strategy to Generate Prime Implicates in Equational Logic
• SOLAR: An automated deduction system for consequence finding
• Prime Implicate Tries
• First order abduction via tableau and sequent calculi
• New results on rewrite-based satisfiability procedures
• RST Flip-Flop Input Equations

This page was built for publication: Quantifier-Free Equational Logic and Prime Implicate Generation