Soft typing for ordered resolution

DOI10.1007/3-540-63104-6_32MaRDI QIDQ5234715zbMATH OpenOpenAlexFDO

Authors Harald Ganzinger, Christoph Meyer, Christoph Weidenbach

Publication date 1 October 2019

Published in Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-63104-6_32

zbMATH Keywords

ground atomground instanceHorn clauseminimal modeltree automaton

Mathematics Subject Classification ID

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

Recommendations

• An order-sorted resolution in theory and practice
• Mizar’s Soft Type System
• Publication:4729409
• Ordered rewriting and confluence
• Residuation for soft constraints: lexicographic orders and approximation techniques
• One modification of the ordering strategy in the resolution method
• Order-sorted inductive types
• Order-sorted unification
• Multi-sorted residuation

Cites work

• Automatic Theorem Proving With Renamable and Semantic Resolution
• Decidable approximations of term rewriting systems
• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• scientific article; zbMATH DE number 1380887 (Why is no real title available?)
• Ordered semantic hyper-linking
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• SPASS \& FLOTTER version 0.42

Cited in

(3)

• Hyperresolution for guarded formulae
• The model evolution calculus as a first-order DPLL method
• MPTP 0.1 -- system description

Describes a project that uses

Uses Software

• SATCHMO
• SPASS
• FLOTTER

This page was built for publication: Soft typing for ordered resolution

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