| ปี พ.ศ. 2556 |
| 1 |
Implementation methodology for using concurrent and collaborative approaches for theorem provers, with case studies of SAT and LCF style provers |
| 2 |
Ontology evolution in physics |
| ปี พ.ศ. 2555 |
| 3 |
Scheme-based theorem discovery and concept invention |
| ปี พ.ศ. 2553 |
| 4 |
Case-Analysis for Rippling and Inductive Proof |
| 5 |
Computational models of ontology evolution in legal reasoning |
| 6 |
Scheme-Based Synthesis of Inductive Theories |
| 7 |
Qualitative Causal Analysis of Empirical Knowledge for Ontology Evolution in Physics |
| 8 |
Formalising Term Synthesis for Isacosy |
| 9 |
Conjecture Synthesis for Inductive Theories |
| 10 |
A Single-Significant-Digit Calculus for Semi-Automated Guesstimation |
| 11 |
Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery |
| 12 |
The AI4FM approach for proof automation within formal methods — A Grand Challenge 6 "Dependable Systems Evolution" project |
| 13 |
A Small Experiement in Event-b Rippling |
| ปี พ.ศ. 2552 |
| 14 |
On Process Equivalence = Equation Solving in CCS |
| 15 |
Isacosy: Synthesis of Inductive Theorems |
| 16 |
Verified Planning by Deductive Synthesis in Intuitionistic Linear Logic |
| 17 |
Automated discovery of inductive lemmas |
| ปี พ.ศ. 2550 |
| 18 |
Cooperating Reasoning Processes: More than Just the Sum of their Parts |
| 19 |
Dynamic, automatic, first-order ontology repair by diagnosis of failed plan execution |
| ปี พ.ศ. 2549 |
| 20 |
HEDGEHOG: Automatic Verification of Design Patterns in Java |
| ปี พ.ศ. 2547 |
| 21 |
Using Diagrammatic Reasoning for Theorem Proving in a Continuous Domain |
| 22 |
The Dynamic Creation of Induction Rules Using Proof Planning |
| 23 |
Diagnosing and Repairing Ontological Mismatches |
| 24 |
An Automatic Translator from KIF to PDDL |
| ปี พ.ศ. 2546 |
| 25 |
Plan Execution Failure Analysis Using Plan Deconstruction |
| 26 |
Attacking the Asokan-Ginzboorg Protocol for Key Distribution in an Ad-Hoc Bluetooth Network Using CORAL |
| ปี พ.ศ. 2543 |
| 27 |
Using Expressive and Flexible Action Representations to Reason about Capabilties for Intelligent Agent Cooperation |
| 28 |
Cross Domain Mathematical Concept Formation |
| ปี พ.ศ. 2542 |
| 29 |
Automating Diagrammatic Proofs of Arithmetic Arguments |
| 30 |
A Survey of Automated Deduction |
| 31 |
Proofs About Lists Using Ellipsis |
| 32 |
The Automation Of Proof By Mathematical Induction |
| 33 |
Making a Productive Use of Failure to Generate Witnesses for Coinduction from Divergent Proof Attempts |
| 34 |
Automatic Concept Formation in Pure Mathematics |
| ปี พ.ศ. 2541 |
| 35 |
Proof Planning Coinduction |
| ปี พ.ศ. 2540 |
| 36 |
Proof Planning for Automating Hardware Verification |
| 37 |
Planning Proofs of Correctness of CCS Systems |
| 38 |
Automation of Diagrammatic Reasoning |
| ปี พ.ศ. 2539 |
| 39 |
Experiments in Automating Hardware Verification using Inductive Proof Planning |
| 40 |
Constructing Probabilistic ATMS Using Extended Incidence Calculus |
| ปี พ.ศ. 2537 |
| 41 |
Coloured rippling: An extension of a theorem proving heuristic |
| 42 |
A Subsumption Architecture for Theorem Proving? |
| 43 |
Proof Plans for the Correction of False Conjectures |
| 44 |
The New Software Copyright Law |
| 45 |
A Comprehensive Comparison between Generalized Incidence Calculus and the Dempster-Shafer Theory of Evidence |
| ปี พ.ศ. 2536 |
| 46 |
`Semantic procedure' is an oxymoron |
| 47 |
General Techniques for Automatic Program Optimization and Synthesis Through Theorem Proving |
| 48 |
A general technique for automatically optimizing programs through the use of proof plans (Extended Abstract) |
| 49 |
Increasing the Versatility of Heuristic Based Theorem Provers |
| 50 |
Rippling: A Heuristic for Guiding Inductive Proofs |
| ปี พ.ศ. 2535 |
| 51 |
Incidence Calculus |
| 52 |
The Use of Proof Plans to Sum Series |
| ปี พ.ศ. 2534 |
| 53 |
Synthesis and Transformation of Logic Programs through Constructive, Inductive Proof |
| 54 |
A Recursive Techniques Editor for Prolog |
| ปี พ.ศ. 2533 |
| 55 |
Turning Eureka Steps into Calculations in Automatic Program Synthesis |
| 56 |
Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs |
| ปี พ.ศ. 2532 |
| 57 |
The ECO Program Construction System: Ways of Increasing its Representational Power and their Effects on the User Interface |
| 58 |
The Use of Prolog for Improving the Rigour and Accessibility of Ecological Modelling |
| 59 |
On the efficiency of meta-level inference |
| ปี พ.ศ. 2531 |
| 60 |
The Use of Explicit Plans to Guide Inductive Proofs |
| ปี พ.ศ. 2530 |
| 61 |
Special Purpose, but Domain Independent, Inference Mechanisms |
| 62 |
AI Bridges and Dreams |
| 63 |
Automated proof search in non-classical logics : efficient matrix proof methods for modal and intuitionistic logics |
| ปี พ.ศ. 2529 |
| 64 |
Correctness criteria of some algorithms for uncertain reasoning using Incidence Calculus |
| ปี พ.ศ. 2528 |
| 65 |
Incidence Calculus: A Mechanism for Probabilistic Reasoning |
| 66 |
Discovery and Reasoning in Mathematics |
| 67 |
Raising the Standard of AI Products |
| ปี พ.ศ. 2527 |
| 68 |
Intelligent Front Ends |
| 69 |
Meta-level Inference and Consciousness |
| 70 |
A Generalized Interval Package and its Use for Semantic Checking |
| ปี พ.ศ. 2525 |
| 71 |
Solving Symbolic Equations with PRESS |
| 72 |
What Is The Well-Dressed AI Educator Wearing Now? |
| ปี พ.ศ. 2524 |
| 73 |
Coping with Uncertainty: Noun Phrase Interpretation and Early Semantic Analysis |
| ปี พ.ศ. 2522 |
| 74 |
Solving Mechanics Problems Using Meta-Level Inference |
| ปี พ.ศ. 2521 |
| 75 |
Will It Reach the Top? Prediction in the Mechanics World. |
| ปี พ.ศ. 2520 |
| 76 |
Representing Semantic Information In Pulley Problems |
