Automatically Proving and Disproving Feasibility Conditions

DOI10.1007/978-3-030-51054-1_27MaRDI QIDQ5049020zbMATH OpenOpenAlexFDO

Authors Raúl Gutiérrez, Salvador Lucas

Publication date 9 November 2022

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-51054-1_27

zbMATH Keywords

conditional rewritingfeasibilityprogram analysis

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Analysis of rewriting-based systems as first-order theories
• Automatic generation of logical models with AGES
• scientific article; zbMATH DE number 1729952 (Why is no real title available?)
• scientific article; zbMATH DE number 4018380 (Why is no real title available?)
• scientific article; zbMATH DE number 1332639 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• Innermost Reachability and Context Sensitive Reachability Properties Are Decidable for Linear Right-Shallow Term Rewriting Systems
• Mechanizing and improving dependency pairs
• MædMax: a maximal ordered completion tool
• Narrowing trees for syntactically deterministic conditional term rewriting systems
• Operational termination of conditional term rewriting systems
• Over-approximating terms reachable by context-sensitive rewriting
• Proving semantic properties as first-order satisfiability
• Reachability Analysis for Termination and Confluence of Rewriting
• Termination of rewriting
• The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
• 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
• Using well-founded relations for proving operational termination

Cited in

(9)

• Applications and extensions of context-sensitive rewriting
• Term orderings for non-reachability of (conditional) rewriting
• mu-term: Verify Termination Properties Automatically (System Description)
• Local confluence of conditional and generalized term rewriting systems
• A Critical Pair Criterion for Level-Commutation of Conditional 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

Describes a project that uses

Uses Software

• Prover9
• Mace4
• ConCon

This page was built for publication: Automatically Proving and Disproving Feasibility Conditions

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