Efficient Low-Level Connection Tableaux

DOI10.1007/978-3-319-24312-2_8zbMath1471.68311OpenAlexW2275159275WikidataQ108482153 ScholiaQ108482153MaRDI QIDQ3455764

Cezary Kaliszyk

Publication date: 11 December 2015

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

Full work available at URL: https://doi.org/10.1007/978-3-319-24312-2_8

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Fast and slow enigmas and parental guidance ⋮ Eliminating models during model elimination ⋮ Craig interpolation with clausal first-order tableaux

Uses Software

• SETHEO
• VAMPIRE
• TPTP
• HOL Light
• E-SETHEO
• MaLeCoP
• iProver
• leanCoP
• randoCoP
• SWI-Prolog

Cites Work

• Unnamed Item
• IeanCOP: lean connection-based theorem proving
• System Description: E 1.8
• SWI-Prolog
• MaLeCoP Machine Learning Connection Prover
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Restricting backtracking in connection calculi
• Constraint Logic Programming Using ECLⁱPS^e
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: Efficient Low-Level Connection Tableaux