Constructing Bachmair-Ganzinger models

DOI10.1007/978-3-642-37651-1_12MaRDI QIDQ4916082zbMATH OpenOpenAlexWikidataFDO

Authors

Publication date 19 April 2013

Published in Programming Logics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-37651-1_12

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 515732
• Model building with ordered resolution: Extracting models from saturated clause sets
• scientific article; zbMATH DE number 549974
• Positive unit hyperresolution tableaux and their application to minimal model generation
• Extracting models from clause sets saturated under semantic refinements of the resolution rule.

Cites work

• scientific article; zbMATH DE number 1696762 (Why is no real title available?)
• A machine program for theorem-proving
• Automated complexity analysis based on ordered resolution
• Automatic recognition of tractability in inference relations
• Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae
• Resolution methods for the decision problem
• Resolution theorem proving
• Termination of rewriting

Cited in

(3)

• Symbolic Model Construction for Saturated Constrained Horn Clauses
• Set of support, demodulation, paramodulation: a historical perspective
• scientific article; zbMATH DE number 2063903 (Why is no real title available?)

This page was built for publication: Constructing Bachmair-Ganzinger models

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