A resolution rule for well-formed formulae

DOI10.1016/0304-3975(91)90192-5zbMATH Open0731.68090OpenAlexW2094992993MaRDI QIDQ808295FDOQ808295

Authors: K. S. H. S. R. Bhatta, Harish Karnick 

Publication date: 1991

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(91)90192-5

Recommendations

• scientific article; zbMATH DE number 4106803
• scientific article; zbMATH DE number 4022664
• scientific article; zbMATH DE number 3871320
• Resolution for quantified monosigned formulae
• Resolution on formula-trees

zbMATH Keywords

interactive theorem provingQ-unificationWFF-resolution

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• A Machine-Oriented Logic Based on the Resolution Principle
• Title not available (Why is that?)
• Title not available (Why is that?)
• Completely non-clausal theorem proving
• Seventy-five problems for testing automatic theorem provers
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (4)

• Resolution for quantified monosigned formulae
• Title not available (Why is that?)
• Title not available (Why is that?)
• Suprema of open and closed formulas and their application to resolution

This page was built for publication: A resolution rule for well-formed formulae

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