Automatic generation of logical models with AGES

DOI10.1007/978-3-030-29436-6_17MaRDI QIDQ2305421zbMATH OpenOpenAlexFDO

Authors 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

abstractionfirst-order logiclogical modelsprogram analysissorts

Mathematics Subject Classification ID

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

Recommendations

• Automatic construction of finite algebras
• Automatic synthesis of logical models for order-sorted first-order theories
• scientific article; zbMATH DE number 2219519
• Symbolic model generation for graph properties
• Generating relevant models

Cites work

• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Automatic synthesis of logical models for order-sorted first-order theories
• Compression of rewriting systems for termination analysis
• Constructing finite algebras with FALCON
• Dependency pairs for proving termination properties of conditional term rewriting systems
• scientific article; zbMATH DE number 1729952 (Why is no real title available?)
• scientific article; zbMATH DE number 4018380 (Why is no real title available?)
• Logic of many-sorted theories
• Matrix interpretations for proving termination of term rewriting
• Mechanizing and improving dependency pairs
• Operational termination of conditional term rewriting systems
• Proving program properties as first-order satisfiability
• Proving termination properties with \textsc{mu-term}
• System description generating models by SEM
• Use of logical models for proving infeasibility in term rewriting
• Using well-founded relations for proving operational termination

Cited in

(11)

• The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
• Proving semantic properties as first-order satisfiability
• AGES
• Automatically Proving and Disproving Feasibility Conditions
• mu-term: Verify Termination Properties Automatically (System Description)
• Local confluence of conditional and generalized term rewriting systems
• Proving confluence in the confluence framework with confident
• Confluence of conditional rewriting modulo
• Confluence of almost parallel-closed generalized term rewriting systems
• Termination of generalized term rewriting systems
• Experiments on infinite model finding in SMT solving

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2305421)