The following pages link to Journal of Automated Reasoning (Q174771):
Displayed 50 items.
- Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction (Q352963) (← links)
- PS\textsc{pace} tableau algorithms for acyclic modalized \({\mathcal{ALC}}\) (Q352965) (← links)
- Simulating circuit-level simplifications on CNF (Q352967) (← links)
- Case splitting in an automatic theorem prover for real-valued special functions (Q352970) (← links)
- Invariant-free clausal temporal resolution (Q352974) (← links)
- Paramodulation with non-monotonic orderings and simplification (Q352977) (← links)
- Reducing equational theories for the decision of static equivalence (Q437026) (← links)
- State and progress in strand spaces: proving fair exchange (Q437028) (← links)
- Decidability of equivalence of symbolic derivations (Q437031) (← links)
- Computing knowledge in security protocols under convergent equational theories (Q437033) (← links)
- Unification modulo homomorphic encryption (Q437037) (← links)
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks (Q437040) (← links)
- The area method. A recapitulation (Q437042) (← links)
- Decidability and combination results for two notions of knowledge in security protocols (Q437043) (← links)
- A combined superposition and model evolution calculus (Q438531) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- Proving termination by dependency pairs and inductive theorem proving (Q438537) (← links)
- Automated inference of finite unsatisfiability (Q438540) (← links)
- Conjecture synthesis for inductive theories (Q438543) (← links)
- A certified proof of the Cartan fixed point theorems (Q438546) (← links)
- Proof pearl: a formal proof of Higman's lemma in ACL2 (Q438550) (← links)
- An interpolating sequent calculus for quantifier-free Presburger arithmetic (Q438556) (← links)
- Monotonicity inference for higher-order formulas (Q438558) (← links)
- Analytic tableaux for higher-order logic with choice (Q438561) (← links)
- Decreasing diagrams and relative termination (Q438562) (← links)
- Tractable extensions of the description logic \({\mathcal{EL}}\) with numerical datatypes (Q438566) (← links)
- Classical logic with partial functions (Q438568) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- A decidability result for the model checking of infinite-state systems (Q438572) (← links)
- SAT modulo linear arithmetic for solving polynomial constraints (Q438576) (← links)
- An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
- Dealing with satisfiability and \(n\)-ary CSPs in a logical framework (Q438582) (← links)
- \(E\)-unification with constants vs. general \(E\)-unification (Q438584) (← links)
- Multi-attacker protocol validation (Q540676) (← links)
- Automated proofs for asymmetric encryption (Q540682) (← links)
- A survey of symbolic methods in computational analysis of cryptographic systems (Q540683) (← links)
- Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach (Q540685) (← links)
- Encoding cryptographic primitives in a calculus with polyadic synchronisation (Q540687) (← links)
- Collaborative planning with confidentiality (Q540688) (← links)
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 (Q540690) (← links)
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling (Q540694) (← links)
- Model-theoretic methods in combined constraint satisfiability (Q556677) (← links)
- A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case (Q556680) (← links)
- On the complexity of deduction modulo leaf permutative equations (Q556681) (← links)
- MPTP-motivation, implementation, first experiments (Q556682) (← links)
- Reachability analysis over term rewriting systems (Q556686) (← links)
- Special issue: First order theorem proving. Selected papers from the 4th workshop, FTP 2003, June 12-14, 2003 (Q556727) (← links)
- Unification under associativity and idempotence is of type nullary (Q580999) (← links)
- The theory of idempotent semigroups is of unification type zero (Q581000) (← links)
- Special issue: Tests and proofs. Selected papers based on the presentations at the 2nd international conference, Prato, Italy, April 2008. (Q604618) (← links)