Nonclausal deduction in first-order temporal logic

DOI10.1145/77600.77617zbMATH Open0696.68096OpenAlexW2057354456MaRDI QIDQ3474286FDOQ3474286

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

Recommendations

• scientific article
• 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

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)

Cited In (20)

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

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)