Hyperresolution for guarded formulae
type: Item
instance of: scholarly article
title: Hyperresolution for guarded formulae
zbMATH Open document ID: 1020.03007
DOI: 10.1016/S0747-7171(03)00034-8
author: Lilia Georgieva
author: Ullrich Hustadt
author: Renate A. Schmidt
published in: Journal of Symbolic Computation
publication date: 2003-08-25T00:00:00Z
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 1970575
zbMATH Keywords: hyperresolution
zbMATH Keywords: decision procedure
zbMATH Keywords: model builder
zbMATH Keywords: guarded fragment
zbMATH Keywords: decidability
zbMATH Keywords: hypertableaux
MaRDI profile type: Publication
cites work: Modal languages and bounded fragments of predicate logic
cites work: Q4860647
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Resolution theorem proving
cites work: Q4282593
cites work: Q3838803
cites work: Q2723420
cites work: Hyper tableaux
cites work: Deciding the guarded fragments by resolution
cites work: Resolution-based methods for modal logics
cites work: Q4514013
cites work: Resolution decision procedures
cites work: Soft typing for ordered resolution
cites work: Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
cites work: Tableau methods for modal and temporal logics
cites work: Q4263155
cites work: On the Restraining Power of Guards
cites work: Q3838813
cites work: Q4503911
cites work: Using resolution for testing modal satisfiability and building models
cites work: Q3142019
cites work: A structure-preserving clause form translation
cites work: Q5541351
cites work: Combining superposition, sorts and splitting
description: scientific article; zbMATH DE number 1970575