Simplification and backjumping in modal tableau

DOI10.1007/3-540-69778-0_22MaRDI QIDQ3838813zbMATH OpenFDO

Authors Ullrich Hustadt, Renate A. Schmidt

Publication date 8 October 1998

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

Full work available at URL https://doi.org/10.1007/3-540-69778-0_22

zbMATH Keywords

backjumpingefficiencymodal logicnondeterminism in tableau calculioptimization techniquessimplification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45)

Review text

The paper is concerned with techniques and strategies aiming to increase the efficiency in dealing with nondeterminism in tableau calculi. A series of preliminary basic definitions and fundamental concepts in modal logic and the difficulties arising from nondeterminism in tableau calculi are recalled in the introductory sections. The main contributions brought by the reported research are given by a simplification technique for modal tableau procedure and backjumping as a means to improve the backtracking behavior of an algorithm, and they are presented in the next two sections of the paper. A series of comments and conclusions concerning the efficiency of the proposed optimization techniques are derived from the empirical analysis of the SICStus Prolog implementations of the calculi MKE, MSKE with simplification and MSKE with backjumping are formulated in the final part of the paper. For the entire collection see [Zbl 0888.00018].

Recommendations

• Simplification: A general constraint propagation technique for propositional and modal tableaux
• Uniform and non uniform strategies for tableaux calculi for modal logics
• scientific article; zbMATH DE number 1552522

Cited in

(6)

• Hyperresolution for guarded formulae
• Rule refinement for semantic tableau calculi
• A prover dealing with nominals, binders, transitivity and relation hierarchies
• A tableaux calculus for default intuitionistic logic
• \textbf{DefTab}: a tableaux system for sceptical consequence in default modal logics
• Constraint learning for non-confluent proof search

This page was built for publication: Simplification and backjumping in modal tableau

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