Nonclausal deduction in first-order temporal logic

DOI10.1145/77600.77617MaRDI QIDQ3474286zbMATH OpenOpenAlexFDO

Authors Martín Abadi, Zohar Manna

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

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

Recommendations

• scientific article; zbMATH DE number 4158604
• A non-reified temporal logic
• scientific article; zbMATH DE number 3904560
• scientific article; zbMATH DE number 22186
• Non-transitive linear temporal logic and logical knowledge operations
• scientific article; zbMATH DE number 4197947
• Nonmonotonic logic and temporal projection
• Natural Deduction Calculus for Linear-Time Temporal Logic
• Executable temporal logic for non-monotonic reasoning
• Non-associative Kleene Algebra and Temporal Logics

Cited in

(20)

• Structured proof procedures
• scientific article; zbMATH DE number 1882041 (Why is no real title available?)
• Removing irrelevant information in temporal resolution proofs
• scientific article; zbMATH DE number 1536570 (Why is no real title available?)
• scientific article; zbMATH DE number 3904560 (Why is no real title available?)
• Decidability and incompleteness results for first-order temporal logics of linear time
• Invariant-free clausal temporal resolution
• Search strategies for resolution in temporal logics
• Embedding complex decision procedures inside an interactive theorem prover.
• First-order temporal verification in practice
• Programming in metric temporal logic
• Non-associative Kleene Algebra and Temporal Logics
• (Heterogeneous) structured specifications in logics without interpolation
• The power of the ``always operator in first-order temporal logic
• Bounded linear-time temporal logic: a proof-theoretic investigation
• Temporal reasoning over linear discrete time
• Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems
• scientific article; zbMATH DE number 3846861 (Why is no real title available?)
• Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic
• scientific article; zbMATH DE number 3972843 (Why is no real title available?)

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

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