Efficient Low-Level Connection Tableaux

DOI10.1007/978-3-319-24312-2_8MaRDI QIDQ3455764zbMATH OpenOpenAlexWikidataFDO

Authors 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)

Recommendations

• Connection Tableaux with Lazy Paramodulation
• Connection tableaux with lazy paramodulation
• Implementing efficient graphs in connection networks
• Efficient lookup on unstructured topologies
• scientific article; zbMATH DE number 1748583
• Efficient graph representations
• Efficient Solution of Connectivity Problems on Hierarchically Defined Graphs
• scientific article; zbMATH DE number 834568
• Publication:4860661

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• Constraint Logic Programming Using ECLⁱPS^e
• IeanCOP: lean connection-based theorem proving
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• MaLeCoP. Machine learning connection prover
• Model elimination and connection tableau procedures
• Restricting backtracking in connection calculi
• SWI-Prolog
• System description: E 1.8

Cited in

(5)

• Eliminating models during model elimination
• Craig interpolation with clausal first-order tableaux
• First-order tableaux in applications (extended abstract)
• Constraint learning for non-confluent proof search
• Fast and slow enigmas and parental guidance

Describes a project that uses

Uses Software

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

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

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