First-order modal tableaux

DOI10.1007/BF00244394zbMath0648.03004OpenAlexW2020852080MaRDI QIDQ1104913

Melvin Fitting

Publication date: 1988

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00244394

zbMATH Keywords

modal logicPrologsemantic tableau based theorem provers

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Related Items (21)

A tableau-like proof procedure for normal modal logics ⋮ Resolution theorem proving in reified modal logics ⋮ Accelerating tableaux proofs using compact representations ⋮ Cut-free sequent and tableau systems for propositional Diodorean modal logics ⋮ The liberalized \(\delta\)-rule in free variable semantic tableaux ⋮ Uniform and non uniform strategies for tableaux calculi for modal logics ⋮ Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems ⋮ MGTP: A model generation theorem prover — Its advanced features and applications — ⋮ Hintikka multiplicities in matrix decision methods for some propositional modal logics ⋮ Labelling ideality and subideality ⋮ The undecidability of simultaneous rigid E-unification ⋮ Proof-terms for classical and intuitionistic resolution ⋮ A simple tableau system for the logic of elsewhere ⋮ On the intuitionistic force of classical search (Extended abstract) ⋮ Building decision procedures for modal logics from propositional decision procedures — The case study of modal K ⋮ A logic for reasoning with inconsistency ⋮ Strongly analytic tableaux for normal modal logics ⋮ Labelled proofs for quantified modal logic ⋮ Decidability and complexity of simultaneous rigid E-unification with one variable and related results ⋮ On the intuitionistic force of classical search ⋮ Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).

This page was built for publication: First-order modal tableaux