Pages that link to "Item:Q1694574"

The following pages link to The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574):

Displayed 49 items.

• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) ‎ (← links)
• Automated deduction and knowledge management in geometry (Q1995808) ‎ (← links)
• A unifying splitting framework (Q2055869) ‎ (← links)
• Superposition with first-class booleans and inprocessing clausification (Q2055873) ‎ (← links)
• Superposition for full higher-order logic (Q2055874) ‎ (← links)
• Neural precedence recommender (Q2055885) ‎ (← links)
• A combinator-based superposition calculus for higher-order logic (Q2096452) ‎ (← links)
• Subsumption demodulation in first-order theorem proving (Q2096454) ‎ (← links)
• SGGS decision procedures (Q2096457) ‎ (← links)
• A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) ‎ (← links)
• Ground joinability and connectedness in the superposition calculus (Q2104507) ‎ (← links)
• SCL(EQ): SCL for first-order logic with equality (Q2104511) ‎ (← links)
• Lash 1.0 (system description) (Q2104521) ‎ (← links)
• \textsf{Goéland}: a concurrent tableau-based theorem prover (system description) (Q2104525) ‎ (← links)
• Bayesian ranking for strategy scheduling in automated theorem provers (Q2104545) ‎ (← links)
• Vampire getting noisy: Will random bits help conquer chaos? (system description) (Q2104552) ‎ (← links)
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (Q2128804) ‎ (← links)
• Towards finding longer proofs (Q2142073) ‎ (← links)
• AC simplifications and closure redundancies in the superposition calculus (Q2142076) ‎ (← links)
• The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics (Q2142078) ‎ (← links)
• Relaxed weighted path order in theorem proving (Q2209265) ‎ (← links)
• A prover dealing with nominals, binders, transitivity and relation hierarchies (Q2303237) ‎ (← links)
• Restricted combinatory unification (Q2305407) ‎ (← links)
• GRUNGE: a grand unified ATP challenge (Q2305410) ‎ (← links)
• Names are not just sound and smoke: word embeddings for axiom selection (Q2305419) ‎ (← links)
• Combining proverif and automated theorem provers for security protocol verification (Q2305427) ‎ (← links)
• Old or heavy? Decaying gracefully with age/weight shapes (Q2305433) ‎ (← links)
• Faster, higher, stronger: E 2.3 (Q2305435) ‎ (← links)
• Extensional higher-order paramodulation in Leo-III (Q2666959) ‎ (← links)
• (Q5018490) ‎ (← links)
• (Q5028439) ‎ (← links)
• Implementing Superposition in iProver (System Description) (Q5049017) ‎ (← links)
• Towards Verifying Logic Programs in the Input Language of clingo (Q5049051) ‎ (← links)
• The CADE-28 Automated Theorem Proving System Competition – CASC-28 (Q5069650) ‎ (← links)
• Formal Qualitative Spatial Augmentation of the Simple Feature Access Model (Q5091722) ‎ (← links)
• Verifying Tight Logic Programs with anthem and vampire (Q5140011) ‎ (← links)
• SAT-Inspired Eliminations for Superposition (Q5875949) ‎ (← links)
• Superposition with lambdas (Q5918381) ‎ (← links)
• Making higher-order superposition work (Q5918403) ‎ (← links)
• Making higher-order superposition work (Q5918575) ‎ (← links)
• Superposition with lambdas (Q5919500) ‎ (← links)
• The 11th IJCAR automated theorem proving system competition – CASC-J11 (Q6095787) ‎ (← links)
• The MET: The Art of Flexible Reasoning with Modalities (Q6104769) ‎ (← links)
• FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets (Q6108818) ‎ (← links)
• SCL(EQ): SCL for first-order logic with equality (Q6111523) ‎ (← links)
• SAT-Inspired Higher-Order Eliminations (Q6135757) ‎ (← links)
• Solving modal logic problems by translation to higher-order logic (Q6139085) ‎ (← links)
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover (Q6156634) ‎ (← links)
• Superposition for higher-order logic (Q6156638) ‎ (← links)