Abstraction-based relevancy testing for model elimination

DOI10.1007/3-540-48660-7_31MaRDI QIDQ4263169zbMATH OpenFDO

Authors M. Fuchs, Dirk Fuchs

Publication date 22 September 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48660-7_31

zbMATH Keywords

formal software verificationsymbol abstractions

Mathematics Subject Classification ID

Recommendations

• A relevance restriction strategy for automated deduction
• scientific article; zbMATH DE number 4164177
• Lightweight relevance filtering for machine-generated resolution problems
• SETHEO goes software engineering: application of ATP to software reuse
• Generating relevant models

Cited in

(8)

• Lightweight relevance filtering for machine-generated resolution problems
• Constructing predicate mappings for goal-dependent abstraction
• An abstraction-refinement framework for reasoning with large theories
• Redundancy-free lemmatization in the automated model-elimination theorem prover AI-SETHEO
• On the relationship between non-Horn magic sets and relevancy testing
• Logic for Programming, Artificial Intelligence, and Reasoning
• Generating relevant models
• A relevance restriction strategy for automated deduction

Describes a project that uses

Uses Software

• SETHEO

This page was built for publication: Abstraction-based relevancy testing for model elimination

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