Prime implicate generation in equational logic

DOI10.1613/JAIR.5481MaRDI QIDQ4600725zbMATH OpenOpenAlexFDO

Authors Mnacho Echenim, Nicolas Peltier, Sophie Tourret

Publication date 12 January 2018

Published in Journal of Artificial Intelligence Research (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1613/jair.5481

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

Recommendations

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

Cited in

(5)

• A generic framework for implicate generation modulo theories
• A rewriting strategy to generate prime implicates in equational logic
• Quantifier-free equational logic and prime implicate generation
• Computing prime implicants via transversal clauses
• An interactive SMT tactic in Coq using abductive reasoning

This page was built for publication: Prime implicate generation in equational logic

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