Pages that link to "Item:Q1823013"

The following pages link to The foundation of a generic theorem prover (Q1823013):

Displaying 23 items.

• Rewriting, and equational unification: the higher-order cases (Q5055746) (← links)
• Higher-order superposition for dependent types (Q5055856) (← links)
• Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL (Q5094474) (← links)
• Proving and rewriting (Q5096184) (← links)
• (Q5140267) (← links)
• Mollusc a general proof-development shell for sequent-based logics (Q5210817) (← links)
• A practical implementation of simple consequence relations using inductive definitions (Q5234714) (← links)
• REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS (Q5249248) (← links)
• Logic-Free Reasoning in Isabelle/Isar (Q5505517) (← links)
• Partiality and recursion in interactive theorem provers – an overview (Q5741556) (← links)
• The practice of logical frameworks (Q5878905) (← links)
• On the Mints Hierarchy in First-Order Intuitionistic Logic (Q5892381) (← links)
• The Watson theorem prover (Q5947358) (← links)
• The control layer in open mechanized reasoning systems: Annotations and tactics (Q5950930) (← links)
• A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
• A formalised theorem in the partition calculus (Q6073894) (← links)
• Semantics for abstract clauses (Q6083702) (← links)
• Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)
• The formal verification of the ctm approach to forcing (Q6151819) (← links)
• Encoding a dependent-type λ-calculus in a logic programming language (Q6488533) (← links)
• A joint logic of problems and propositions (Q6575364) (← links)
• Formalizing Pick's theorem in Isabelle/HOL (Q6648161) (← links)
• Formalizing Coppersmith's method in Isabelle/HOL (Q6648162) (← links)