Interactive proof-search for equational reasoning

DOI10.1093/JIGPAL/JZAA013MaRDI QIDQ3386920zbMATH OpenOpenAlexFDO

Authors Favio E. Miranda Perea, Lourdes del Carmen González Huesca, P. Selene Linares-Arévalo

Publication date 8 January 2021

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/jzaa013

zbMATH Keywords

Birkhoff calculusequational logicgoal-oriented reasoningproof-searchrewrite

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Proof search and proof check for equational and inductive theorems.
• scientific article; zbMATH DE number 4035205
• scientific article; zbMATH DE number 50648
• Equational reasoning in Isabelle
• Artificial Intelligence and Symbolic Computation

Cited in

(2)

• scientific article; zbMATH DE number 4035205 (Why is no real title available?)
• A two-level approach towards lean proof-checking

Describes a project that uses

Uses Software

• Maude
• Coq
• Haskell

This page was built for publication: Interactive proof-search for equational reasoning

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