A practical integration of first-order reasoning and decision procedures

DOI10.1007/3-540-63104-6_13zbMath1430.03037OpenAlexW1602383075MaRDI QIDQ5234694

T. E. Uribe, Mark E. Stickel, Nikolaj Bjørner

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_13

zbMATH Keywords

formal verificationsequent calculuspartial orderdecision procedureverification condition

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Constraint contextual rewriting. ⋮ Deductive verification of real-time systems using STeP

Uses Software

• PVS
• STeP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The undecidability of simultaneous rigid E-unification
• The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
• Deductive verification of real-time systems using STeP
• A resolution principle for a logic with restricted quantifiers
• Automated deduction by theory resolution
• Branching rules for satisfiability
• Temporal Verification of Reactive Systems: Response
• Deciding Combinations of Theories
• Fast Decision Procedures Based on Congruence Closure
• Theorem Proving via General Matings
• Theorem proving using equational matings and rigid E -unification
• On Shostak's decision procedure for combinations of theories
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving

This page was built for publication: A practical integration of first-order reasoning and decision procedures