Soft typing for ordered resolution

DOI10.1007/3-540-63104-6_32zbMath1430.68407OpenAlexW2132897607MaRDI QIDQ5234715

Christoph Weidenbach, Christoph Meyer, Harald Ganzinger

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

minimal modeltree automatonHorn clauseground instanceground atom

Mathematics Subject Classification ID

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

Related Items (3)

The model evolution calculus as a first-order DPLL method ⋮ Hyperresolution for guarded formulae ⋮ MPTP 0.1 - System Description

Uses Software

• SPASS
• SATCHMO
• FLOTTER

Cites Work

• Ordered semantic hyper-linking
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• SPASS & FLOTTER version 0.42
• Decidable approximations of term rewriting systems
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Unnamed Item
• Unnamed Item

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