Stratified resolution

DOI10.1016/S0747-7171(03)00036-1zbMath1024.03013OpenAlexW2911964946MaRDI QIDQ1404977

Andrei Voronkov, Anatoli Degtyarev, Robert Nieuwenhuis

Publication date: 25 August 2003

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0747-7171(03)00036-1

zbMATH Keywords

first-order logicautomated theorem provingredundancy eliminationdefinition unfoldingordered resolution with selection

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (3)

On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction

Uses Software

• VAMPIRE
• Saturate

Cites Work

• Simple LPO constraint solving methods
• Oriented equational logic programming is complete
• Linear resolution with selection function
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Stratified resolution