A First Class Boolean Sort in First-Order Theorem Proving and TPTP

DOI10.1007/978-3-319-20615-8_5zbMath1417.68187arXiv1505.01682OpenAlexW1728498852MaRDI QIDQ3453107

Evgenii Kotelnikov, Andrei Voronkov, Laura Kovács

Publication date: 20 November 2015

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

Full work available at URL: https://arxiv.org/abs/1505.01682

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Improving automation for higher-order proof steps ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ FOOL

Uses Software

• Isabelle/HOL
• VAMPIRE
• SMT-LIB
• SPASS
• TPTP
• z3
• MML
• Sledgehammer
• CVC4
• iProver
• E Theorem Prover
• Lingva

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• System Description: E 1.8
• The TPTP Typed First-Order Form with Arithmetic
• Playing in the grey area of proofs
• Lingva: Generating and Proving Program Properties Using Symbol Elimination
• Extensional Crisis and Proving Identity
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Superposition for Bounded Domains
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Sledgehammer: Judgement Day
• Evaluation of Automated Theorem Proving on the Mizar Mathematical Library