Proving semantic properties as first-order satisfiability
From MaRDI portal
Publication:2289018
Recommendations
- Analysis of rewriting-based systems as first-order theories
- Satisfiability calculus: the semantic counterpart of a proof calculus in general logics
- Semantic Guidance for Saturation Provers
- Satisfiability calculus: an abstract formulation of semantic proof systems
- Foundations of satisfiability modulo theories
Cites work
- scientific article; zbMATH DE number 1729952 (Why is no real title available?)
- scientific article; zbMATH DE number 4018380 (Why is no real title available?)
- scientific article; zbMATH DE number 1805574 (Why is no real title available?)
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- scientific article; zbMATH DE number 53151 (Why is no real title available?)
- scientific article; zbMATH DE number 3529405 (Why is no real title available?)
- scientific article; zbMATH DE number 1257634 (Why is no real title available?)
- scientific article; zbMATH DE number 1765702 (Why is no real title available?)
- scientific article; zbMATH DE number 781332 (Why is no real title available?)
- scientific article; zbMATH DE number 6792369 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- A relational model of data for large shared data banks
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Analysis of rewriting-based systems as first-order theories
- Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation
- Automatic generation of logical models with AGES
- Automatic synthesis of logical models for order-sorted first-order theories
- Certifying confluence of almost orthogonal CTRSs via exact tree automata completion
- Conditional rewriting logic as a unified model of concurrency
- Context-sensitive rewriting strategies
- Disproving confluence of term rewriting systems by interpretation and ordering
- Equality and Domain Closure in First-Order Databases
- Finding Finite Models in Multi-sorted First-Order Logic
- Finite Models in FOL-Based Crypto-Protocol Verification
- Finite Models vs Tree Automata in Safety Verification
- Finite reasons for safety. Parameterized verification by finite model finding
- Functional Dependencies in a Relational Database and Propositional Logic
- Lazy productivity via termination
- Logic of many-sorted theories
- Models for an adversary-centric protocol logic
- Operational termination of conditional term rewriting systems
- Proof by consistency
- Properties of Programs and the First-Order Predicate Calculus
- Proving program properties as first-order satisfiability
- Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
- Semantic foundations for generalized rewrite theories
- System description generating models by SEM
- The Semantics of Predicate Logic as a Programming Language
- The execution algorithm of mercury, an efficient purely declarative logic programming language
- The first-order theory of linear one-step rewriting is undecidable
- Use of logical models for proving infeasibility in term rewriting
Cited in
(9)- Semantic Guidance for Saturation Provers
- Automatically Proving and Disproving Feasibility Conditions
- mu-term: Verify Termination Properties Automatically (System Description)
- Proving program properties as first-order satisfiability
- Local confluence of conditional and generalized term rewriting systems
- Exploring theories with a model-finding assistant
- Many-valued logic and sequence arguments in value theory
- Proving confluence in the confluence framework with confident
- Analysis of rewriting-based systems as first-order theories
This page was built for publication: Proving semantic properties as first-order satisfiability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2289018)
