Constrained hyper tableaux

DOI10.1007/3-540-44802-0_17MaRDI QIDQ4783311zbMATH OpenFDO

Authors Jan van Eijck

Publication date 4 December 2002

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2142/21420232

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Recommendations

• Hyper tableaux
• Hyper tableau -- the next generation
• Ordered tableaux: extensions and applications
• scientific article; zbMATH DE number 1552524
• scientific article; zbMATH DE number 2219496

Cited in

(9)

• The model evolution calculus as a first-order DPLL method
• Introducing general redundancy criteria for clausal tableaux, and proposing resolution tableaux
• Hyper tableau -- the next generation
• Model generation and existentially quantified variables and constraints
• scientific article; zbMATH DE number 1552524 (Why is no real title available?)
• Simplification rules for constrained formula tableaux
• Fair constraint merging tableaux in lazy functional programming style
• Hyper tableaux
• Automated Deduction – CADE-20

Describes a project that uses

Uses Software

• Haskell

This page was built for publication: Constrained hyper tableaux

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