Computational Space Efficiency and Minimal Model Generation for Guarded Formulae

DOI10.1007/3-540-45653-8_6MaRDI QIDQ2996155zbMATH OpenOpenAlexFDO

Authors Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt

Publication date 6 May 2011

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-45653-8_6

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Modal logic (including the logic of norms) (03B45) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in artificial intelligence (68T27)

Recommendations

• A model of guarded recursion via generalised equilogical spaces
• An application of model building in a resolution decision procedure for guarded formulas
• Space-reduction strategies for model checking dynamic software
• The complexity of model checking for circumscriptive formulae
• A framework for space complexity in algebraic proof systems
• Efficient minimal model generation using branching lemmas
• scientific article; zbMATH DE number 1418459
• Symbolic model checking with fewer fixpoint computations
• Resource-constrained model checking of recursive programs

Cited in

(6)

• A new methodology for developing deduction methods
• Hyperresolution for guarded formulae
• A model of guarded recursion via generalised equilogical spaces
• An application of model building in a resolution decision procedure for guarded formulas
• A tableau calculus for minimal modal model generation
• First-order resolution methods for modal logics

This page was built for publication: Computational Space Efficiency and Minimal Model Generation for Guarded Formulae

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