Subgoal alternation in model elimination

DOI10.1007/BFb0027415zbMath1412.68237OpenAlexW1497982119MaRDI QIDQ4610327

Ortrun Ibens, Reinhold Letz

Publication date: 15 January 2019

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

Full work available at URL: https://doi.org/10.1007/bfb0027415

zbMATH Keywords

automated deductionchoice pointunit clausemodel eliminationunification partner

Mathematics Subject Classification ID

Related Items (1)

Towards the qualitative, plan-based simulation of international crises

Uses Software

• SETHEO
• TPTP
• E-SETHEO

Cites Work

• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• SETHEO: A high-performance theorem prover
• Refutation graphs
• Controlled integration of the cut rule into connection tableau calculi
• Proving Theorems with the Modification Method
• Optimizing proof search in model elimination
• The TPTP problem library
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Subgoal alternation in model elimination