SAT-Inspired Higher-Order Eliminations

DOI10.46298/lmcs-19(2:9)2023arXiv2208.07775OpenAlexW4375860224MaRDI QIDQ6135757

Jasmin Christian Blanchette, Petar Vukmirović

Publication date: 26 August 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Types, tableaus, and Gödel's God
• Isabelle/HOL. A proof assistant for higher-order logic
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• The higher-order prover Leo-III
• Superposition for full higher-order logic
• A combinator-based superposition calculus for higher-order logic
• Extensional higher-order paramodulation in Leo-III
• Predicate Elimination for Preprocessing in First-Order Theorem Proving
• Efficient CNF Simplification Based on Binary Implication Graphs
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• SCAN—Elimination of predicate quantifiers
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• SAT-Inspired Eliminations for Superposition
• Making higher-order superposition work

This page was built for publication: SAT-Inspired Higher-Order Eliminations