Automatic synthesis of logical models for order-sorted first-order theories

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

zbMATH Keywords

program analysislogical modelsorder-sorted first-order logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

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

• OBJ3
• CafeOBJ
• Maude
• Matchbox
• SeaHorn
• GitHub

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 Π₁¹ 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