Connection tableau calculi with disjunctive constraints

DOI10.1023/A:1015134701251MaRDI QIDQ1604795zbMATH OpenFDO

Authors Ortrun Ibens

Publication date 8 July 2002

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/A:1015134701251

zbMATH Keywords

automated connection tableau prover SETHEOconstrained-connection-tableau calculifirst-order automated theorem provingfirst-order constraint solvingsearch space reduction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1612557
• Connection tableau calculi with disjunctive contraints (TU München)
• Controlled use of clausal lemmas in connection tableau calculi
• The disconnection method
• The disconnection tableau calculus

Cited in

(3)

• scientific article; zbMATH DE number 1612557 (Why is no real title available?)
• Connection tableau calculi with disjunctive contraints (TU München)
• Restricting backtracking in connection calculi

Describes a project that uses

Uses Software

• SETHEO
• TPTP

This page was built for publication: Connection tableau calculi with disjunctive constraints

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