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

DOI10.1093/LOGCOM/EXN061MaRDI QIDQ3406685zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

automated reasoningequalityfinite model computationhyper tableaux

Mathematics Subject Classification ID

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

Recommendations

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

Cited in

(13)

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

Describes a project that uses

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)