scientific article; zbMATH DE number 1950259

zbMath1015.03011MaRDI QIDQ4412857

Jan Hladík

Publication date: 17 July 2003

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2381/23810145.htm

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments ⋮ Optimizing terminological reasoning for expressive description logics ⋮ A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders ⋮ A prover dealing with nominals, binders, transitivity and relation hierarchies ⋮ Deciding regular grammar logics with converse through first-order logic ⋮ A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities

Uses Software

• SPASS