Constructing Bachmair-Ganzinger models

DOI10.1007/978-3-642-37651-1_12zbMATH Open1383.68079OpenAlexW84077869WikidataQ118190379 ScholiaQ118190379MaRDI QIDQ4916082FDOQ4916082

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

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.

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Resolution theorem proving
• A machine program for theorem-proving
• Termination of rewriting
• Automatic recognition of tractability in inference relations
• Automated complexity analysis based on ordered resolution
• Resolution methods for the decision problem
• Title not available (Why is that?)
• Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae

Cited In (3)

• Set of support, demodulation, paramodulation: a historical perspective
• Title not available (Why is that?)
• Symbolic Model Construction for Saturated Constrained Horn Clauses

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)