The following pages link to (Q4726218):
Displaying 40 items.
- ETPS (Q18433) (← links)
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
- Probabilistic modelling, inference and learning using logical theories (Q841641) (← links)
- On connections and higher-order logic (Q908896) (← links)
- Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems (Q916414) (← links)
- Rigid E-unification: NP-completeness and applications to equational matings (Q921913) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- Abstract deduction and inferential models for type theory (Q988551) (← links)
- Data types with errors and exceptions (Q1196304) (← links)
- Unification under a mixed prefix (Q1201348) (← links)
- Universal abstract consistency class and universal refutation (Q1288438) (← links)
- Experimenting with Isabelle in ZF set theory (Q1312157) (← links)
- What holds in a context? (Q1312161) (← links)
- Combinatory reduction systems: Introduction and survey (Q1314356) (← links)
- A simple type theory with partial functions and subtypes (Q1314643) (← links)
- IMPS: An interactive mathematical proof system (Q1319391) (← links)
- A semantics for \(\lambda \)Prolog (Q1349686) (← links)
- Using tactics to reformulate formulae for resolution theorem proving (Q1380410) (← links)
- Quantum number theory (Q1770337) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- Higher-order unification revisited: Complete sets of transformations (Q1823936) (← links)
- Higher order unification via explicit substitutions (Q1854337) (← links)
- Computing verisimilitude (Q1903577) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Decidability of fluted logic with identity (Q1924331) (← links)
- Grammar induction by unification of type-logical lexicons (Q1959226) (← links)
- A survey of nonstandard sequent calculi (Q2259014) (← links)
- Completeness in equational hybrid propositional type theory (Q2278838) (← links)
- Probabilistic reasoning in a classical logic (Q2390656) (← links)
- Decidability of bounded higher-order unification (Q2456577) (← links)
- Combining Model Checking and Deduction (Q3176378) (← links)
- HOL Light: An Overview (Q3183517) (← links)
- General framework of structural similarity between system models (Q3356149) (← links)
- 2004 Summer Meeting of the Association for Symbolic Logic (Q3370624) (← links)
- Identity, equality, nameability and completeness. Part II (Q4629288) (← links)
- On sets, types, fixed points, and checkerboards (Q4645222) (← links)
- Rewriting, and equational unification: the higher-order cases (Q5055746) (← links)
- A logical framework combining model and proof theory (Q5400853) (← links)
- A partial functions version of Church's simple theory of types (Q5753924) (← links)
- MBase: Representing knowledge and context for the integration of mathematical software systems (Q5950933) (← links)
