Quantifier-free equational logic and prime implicate generation

DOI10.1007/978-3-319-21401-6_21MaRDI QIDQ3454103zbMATH OpenOpenAlexFDO

Authors Mnacho Echenim, Nicolas Peltier, Sophie Tourret

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)

Recommendations

• Prime implicate generation in equational logic
• A rewriting strategy to generate prime implicates in equational logic
• A generic framework for implicate generation modulo theories
• scientific article; zbMATH DE number 1390353
• An efficient algorithm to generate prime implicants

Cites work

• A rewriting strategy to generate prime implicates in equational logic
• An incremental method for generating prime implicants/implicates
• Equality and abductive residua for Horn clauses
• First order abduction via tableau and sequent calculi
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 1348482 (Why is no real title available?)
• scientific article; zbMATH DE number 1390353 (Why is no real title available?)
• Implication of clauses is undecidable
• New results on rewrite-based satisfiability procedures
• Paramodulation-based theorem proving
• Prime implicate tries
• RST Flip-Flop Input Equations
• SOLAR: An automated deduction system for consequence finding
• System description: E 1.8
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Theory decision by decomposition

Cited in

(5)

• A generic framework for implicate generation modulo theories
• Logical reduction of metarules
• A rewriting strategy to generate prime implicates in equational logic
• Prime implicates and prime implicants: from propositional to modal logic
• Prime implicate generation in equational logic

Describes a project that uses

Uses Software

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

This page was built for publication: Quantifier-free equational logic and prime implicate generation

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