The following pages link to (Q4863622):
Displaying 50 items.
- An intensional type theory: Motivation and cut-elimination (Q2732287) (← links)
- A proof-planning framework with explicit abstractions based on indexed formulas (Q2841241) (← links)
- Decision Procedures for Region Logic (Q2891431) (← links)
- Exact Query Reformulation with First-Order Ontologies and Databases (Q2915072) (← links)
- A Unifying Perspective on Knowledge Updates (Q2915086) (← links)
- Approximating Beppo Levi's \textit{principio di approssimazione} (Q2925330) (← links)
- Simulating Dynamic Systems Using Linear Time Calculus Theories (Q2931258) (← links)
- Free Variables and Theories: Revisiting Rigid E-unification (Q2964448) (← links)
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Q3075472) (← links)
- Interpolation for first order S5 (Q3149986) (← links)
- Extended First-Order Logic (Q3183527) (← links)
- CUT AND GAMMA I: PROPOSITIONAL AND CONSTANT DOMAIN <b>R</b> (Q3389499) (← links)
- Intensional models for the theory of types (Q3426565) (← links)
- Theorem Proving with Bounded Rigid E-Unification (Q3454123) (← links)
- Efficient Algorithms for Bounded Rigid E-unification (Q3455762) (← links)
- On Enumerating Query Plans Using Analytic Tableau (Q3455780) (← links)
- (Q3996619) (← links)
- (Q4014783) (← links)
- Infinite-Valued First-Order Łukasiewicz Logic: Hypersequent Calculi Without Structural Rules and Proof Search for Sentences in the Prenex Form (Q4558324) (← links)
- (Q4575567) (← links)
- Lean induction principles for tableaux (Q4610315) (← links)
- Free variable tableaux for propositional modal logics (Q4610317) (← links)
- Non-elementary speed-ups in proof length by different variants of classical analytic calculi (Q4610324) (← links)
- Ordered tableaux: Extensions and applications (Q4610325) (← links)
- A framework for using knowledge in tableau proofs (Q4610337) (← links)
- Minimal model generation with positive unit hyper-resolution tableaux (Q4645233) (← links)
- The tableau-based theorem prover 3 T A P Version 4.0 (Q4647529) (← links)
- Reasoning with Uncertain and Inconsistent OWL Ontologies (Q4647816) (← links)
- The lazy logic of partial terms (Q4779651) (← links)
- (Q4989394) (← links)
- Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL (Q5206953) (← links)
- Stoic Sequent Logic and Proof Theory (Q5208124) (← links)
- Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis (Q5215504) (← links)
- A semantics for nabla (Q5236555) (← links)
- Higher-order semantics and extensionality (Q5311767) (← links)
- Many-Valued Non-deterministic Semantics for First-Order Logics of Formal (In)consistency (Q5425994) (← links)
- KeY: A Formal Method for Object-Oriented Systems (Q5428904) (← links)
- Towards the Formal Reliability Analysis of Oil and Gas Pipelines (Q5495912) (← links)
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic (Q5504659) (← links)
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic (Q5747778) (← links)
- SAT-Inspired Eliminations for Superposition (Q5875949) (← links)
- Controlled use of clausal lemmas in connection tableau calculi (Q5927985) (← links)
- Tableau methods for a logic with term declarations (Q5927986) (← links)
- Connection calculus theorem proving with multiple built-in theories (Q5927987) (← links)
- Reasoning on with Defeasibility in ASP (Q6063881) (← links)
- Local confluence of conditional and generalized term rewriting systems (Q6151615) (← links)
- Range-restricted and Horn interpolation through clausal tableaux (Q6541142) (← links)
- Deduction by combining semantic tableaux and integer programming (Q6560161) (← links)
- Reasoning with preorders and dynamic sorts using free variable tableaux (Q6560387) (← links)
- Tableaux and interpolation for propositional justification logics (Q6564678) (← links)
