Nonclausal deduction in first-order temporal logic

DOI10.1145/77600.77617zbMath0696.68096OpenAlexW2057354456MaRDI QIDQ3474286

Zohar Manna, Martín Abadi

Publication date: 1990

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/77600.77617

zbMATH Keywords

automated deductionfirst-order temporal logicconcurrent-program verificationnonclausal resolution

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35)

Related Items (12)

The power of the ``always operator in first-order temporal logic ⋮ Decidability and incompleteness results for first-order temporal logics of linear time ⋮ Embedding complex decision procedures inside an interactive theorem prover. ⋮ Invariant-free clausal temporal resolution ⋮ Structured proof procedures ⋮ Programming in metric temporal logic ⋮ Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic ⋮ Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems ⋮ Search strategies for resolution in temporal logics ⋮ Removing irrelevant information in temporal resolution proofs ⋮ Bounded linear-time temporal logic: a proof-theoretic investigation ⋮ Temporal reasoning over linear discrete time

This page was built for publication: Nonclausal deduction in first-order temporal logic