Proving semantic properties as first-order satisfiability
From MaRDI portal
Publication:2289018
DOI10.1016/J.ARTINT.2019.103174zbMATH Open1478.68356OpenAlexW2973608737MaRDI QIDQ2289018FDOQ2289018
Authors: Salvador Lucas 
Publication date: 20 January 2020
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/10251/139771
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
Logic programming (68N17) Database theory (68P15) Grammars and rewriting systems (68Q42) Logic in artificial intelligence (68T27) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Automatic generation of logical models with AGES
- Title not available (Why is that?)
- Title not available (Why is that?)
- A relational model of data for large shared data banks
- The Semantics of Predicate Logic as a Programming Language
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- Title not available (Why is that?)
- Functional Dependencies in a Relational Database and Propositional Logic
- Title not available (Why is that?)
- Operational termination of conditional term rewriting systems
- Conditional rewriting logic as a unified model of concurrency
- Analysis of rewriting-based systems as first-order theories
- Semantic foundations for generalized rewrite theories
- Title not available (Why is that?)
- Automatic synthesis of logical models for order-sorted first-order theories
- Proof by consistency
- Context-sensitive rewriting strategies
- Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
- Lazy productivity via termination
- Title not available (Why is that?)
- Equality and Domain Closure in First-Order Databases
- Proving program properties as first-order satisfiability
- Finite Models vs Tree Automata in Safety Verification
- Properties of Programs and the First-Order Predicate Calculus
- Logic of many-sorted theories
- The execution algorithm of mercury, an efficient purely declarative logic programming language
- Title not available (Why is that?)
- Models for an adversary-centric protocol logic
- Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation
- Title not available (Why is that?)
- Title not available (Why is that?)
- The first-order theory of linear one-step rewriting is undecidable
- Use of logical models for proving infeasibility in term rewriting
- Disproving confluence of term rewriting systems by interpretation and ordering
- Certifying confluence of almost orthogonal CTRSs via exact tree automata completion
- Finding Finite Models in Multi-sorted First-Order Logic
- Title not available (Why is that?)
- Finite reasons for safety. Parameterized verification by finite model finding
- Finite Models in FOL-Based Crypto-Protocol Verification
- System description generating models by SEM
Cited In (9)
- 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
- Semantic Guidance for Saturation Provers
Uses Software
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)
