Deciding the E^+-class by an a posteriori, liftable order

DOI10.1016/S0168-0072(00)00013-0zbMATH Open0966.03012OpenAlexW2010309877WikidataQ127592956 ScholiaQ127592956MaRDI QIDQ1577484FDOQ1577484

Authors: Hans de Nivelle 

Publication date: 26 July 2001

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(00)00013-0

Recommendations

• scientific article; zbMATH DE number 512974
• Resolution decision procedures
• Publication:4942004

zbMATH Keywords

decidable classestheorem-proving\(E^+\)-classliftable order

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Cites Work

• A Machine-Oriented Logic Based on the Resolution Principle
• Title not available (Why is that?)
• On a bound for the complexity of terms in the resolution method
• Title not available (Why is that?)
• Resolution Strategies as Decision Procedures
• Title not available (Why is that?)
• Resolution methods for the decision problem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (2)

• A classification of non-liftable orders for resolution
• A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).

Uses Software

• OTTER
• SPASS
• FLOTTER

This page was built for publication: Deciding the \(E^+\)-class by an a posteriori, liftable order

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