Automatic synthesis of logical models for order-sorted first-order theories
From MaRDI portal
Publication:1655487
DOI10.1007/S10817-017-9419-3zbMath1398.68095OpenAlexW2734627336MaRDI QIDQ1655487
Salvador Lucas, Raúl Gutiérrez
Publication date: 9 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/10251/124228
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (11)
mu-term: Verify Termination Properties Automatically (System Description) ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Use of logical models for proving infeasibility in term rewriting ⋮ Proving semantic properties as first-order satisfiability ⋮ Using well-founded relations for proving operational termination ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ Automatic generation of logical models with AGES ⋮ Tuple interpretations for termination of term rewriting
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Proving termination by dependency pairs and inductive theorem proving
- SAT modulo linear arithmetic for solving polynomial constraints
- Mechanically proving termination using polynomial interpretations
- Matrix interpretations for proving termination of term rewriting
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Operational termination of conditional term rewriting systems
- Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories
- Some fundamental algebraic tools for the semantics of computation: II. Signed and abstract theories
- A mechanical solution of Schubert's steamroller by many-sorted resolution
- Counterexamples to termination for the direct sum of term rewriting systems
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Termination of term rewriting: Interpretation and type elimination
- On Skolemization in constrained logics
- Computational aspects of an order-sorted logic with term declarations
- Automatic program verification. I: A logical basis and its implementation
- Synthesis of sup-interpretations: a survey
- Use of Logical Models for Proving Operational Termination in General Logics
- Sup-interpretations, a semantic method for static analysis of program resources
- Horn Clause Solvers for Program Verification
- Order-sorted termination: The unsorted way
- The Reduced Product of Abstract Domains and the Combination of Decision Procedures
- Transition Invariants and Transition Predicate Abstraction for Program Termination
- Proving Termination Properties with mu-term
- Theory of Formal Systems. (AM-47)
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Improved Matrix Interpretation
- A Transformational Approach to Resource Analysis with Typed-Norms
- Termination Competition (termCOMP 2015)
- Maximal Termination
- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
- Automated Complexity Analysis Based on the Dependency Pair Method
- Matrix Interpretations for Proving Termination of Term Rewriting
- A Practical Decision Procedure for Arithmetic with Function Symbols
- Axioms for abstract model theory
- The Semantics of Predicate Logic as a Programming Language
- Logical analysis of programs
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Termination proofs and the length of derivations
- Matrix Interpretations on Polyhedral Domains.
- Polynomials over the reals in proofs of termination : from theory to practice
- Revisiting Matrix Interpretations for Proving Termination of Term Rewriting
- Automated Termination Analysis of Java Bytecode by Term Rewriting
- An axiomatic basis for computer programming
- Properties of Programs and the First-Order Predicate Calculus
- Formalization of Properties of Functional Programs
- Heterogeneous algebras
- Applications of Strict Π11 predicates to infinitary logic
- Recent Trends in Algebraic Development Techniques
- Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras
- Logic of many-sorted theories
- Termination proofs for ground rewrite systems -- interpretations and derivational complexity
This page was built for publication: Automatic synthesis of logical models for order-sorted first-order theories
