A resolution-based decision procedure for the two-variable fragment with equality

DOI10.1007/3-540-45744-5_16MaRDI QIDQ4539607zbMATH OpenFDO

Authors Hans de Nivelle, Ian Pratt-Hartmann

Publication date 10 July 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2083/20830211

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

Recommendations

• The two-variable fragment with counting and equivalence
• On the Decision Problem for Two-Variable First-Order Logic
• Two variables and two successors
• The two-variable fragment with counting revisited
• On logics with two variables

Cited in

(5)

• Deciding regular grammar logics with converse through first-order logic
• A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$
• Using tableau to decide description logics with full role negation and identity
• A description logic based situation calculus
• A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).

This page was built for publication: A resolution-based decision procedure for the two-variable fragment with equality

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