The hyper tableaux calculus with equality and an application to finite model computation

DOI10.1093/LOGCOM/EXN061zbMATH Open1193.03025OpenAlexW2135088169MaRDI QIDQ3406685FDOQ3406685

Authors: Peter Baumgartner, Björn Pelzer, Ulrich Furbach 

Publication date: 19 February 2010

Published in: Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exn061

Recommendations

• scientific article; zbMATH DE number 2219496
• Hyper Tableaux with Equality
• Hyper tableaux
• scientific article; zbMATH DE number 1189096
• Connection Tableaux with Lazy Paramodulation

zbMATH Keywords

equalityautomated reasoningfinite model computationhyper tableaux

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Mechanization of proofs and logical operations (03B35)

Cited In (13)

• Blocking and other enhancements for bottom-up model generation methods
• Set of support, demodulation, paramodulation: a historical perspective
• Title not available (Why is that?)
• Title not available (Why is that?)
• Superposition for bounded domains
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• Connection Tableaux with Lazy Paramodulation
• Title not available (Why is that?)
• Superposition-based equality handling for analytic tableaux
• On First-Order Model-Based Reasoning
• Connection tableaux with lazy paramodulation
• Hyper Tableaux with Equality
• HyperS tableaux -- heuristic hyper tableaux

Uses Software

• TPTP
• SATCHMO
• Mace4

This page was built for publication: The hyper tableaux calculus with equality and an application to finite model computation

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