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

DOI10.1016/S0168-0072(00)00013-0MaRDI QIDQ1577484zbMATH OpenOpenAlexWikidataFDO

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

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)

Recommendations

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

Cites work

• scientific article; zbMATH DE number 4200168 (Why is no real title available?)
• scientific article; zbMATH DE number 3961574 (Why is no real title available?)
• scientific article; zbMATH DE number 3715502 (Why is no real title available?)
• scientific article; zbMATH DE number 1303345 (Why is no real title available?)
• scientific article; zbMATH DE number 976360 (Why is no real title available?)
• scientific article; zbMATH DE number 2079034 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• On a bound for the complexity of terms in the resolution method
• Resolution Strategies as Decision Procedures
• Resolution methods for the decision problem

Cited in

(2)

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

Describes a project that uses

Uses Software

• FLOTTER
• SPASS
• OTTER

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)