Automatic generation of logical models with AGES

DOI10.1007/978-3-030-29436-6_17OpenAlexW2969868654MaRDI QIDQ2305421

Raúl Gutiérrez, Salvador Lucas

Publication date: 10 March 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-29436-6_17

zbMATH Keywords

first-order logicsortsprogram analysisabstractionlogical models

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

Automatically Proving and Disproving Feasibility Conditions ⋮ mu-term: Verify Termination Properties Automatically (System Description) ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Proving semantic properties as first-order satisfiability ⋮ AGES

Uses Software

• Yices
• z3
• Prover9
• Maude
• Mace4
• FALCON

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependency pairs for proving termination properties of conditional term rewriting systems
• Mechanizing and improving dependency pairs
• 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
• Constructing finite algebras with FALCON
• Automatic synthesis of logical models for order-sorted first-order theories
• Use of logical models for proving infeasibility in term rewriting
• Using well-founded relations for proving operational termination
• Proving Termination Properties with mu-term
• System description generating models by SEM
• Logic of many-sorted theories
• Proving program properties as first-order satisfiability

This page was built for publication: Automatic generation of logical models with AGES