KWTR: first-order logic

[edit] Contributors:

Jos de Bruijn, FUB

Please add your CV in the list of contributors

First-order logic is a well established formalism, and is the basis for many other subfields such as Description Logics and logic programming.

• 1. CURRENT TRENDS IN SEMANTIC WEB (In the following part we intend to identify the state of the art of Semantic Web based theories, methods, applications and tools in your research field.)

• • 1.1. One or more examples (case studies) in which semantic web has been used.

  Name of the institutions:
  Industry / sector: 
  Business activities improved by the SW solutions: 
  Research Needs: 
  Name of the project:
  Tools and applications implemented in the project:

• • 1.2. The first 4 Semantic Web based tools used in your research fields.

Name: 
Website: 
Main characteristics:  
Open problems: 

• • 1.3. A short summary of the first 3 best papers in the field.

Reference:  Melvin Fitting. First Order Logic and Automated Theorem Proving 
(second edition). Springer Verlag, 1996.
Short abstract: This graduate-level text presents fundamental concepts and   
results of classical logic in a rigorous mathematical style. Applications to  
automated theorem proving are considered and usable Prolog programs provided. It 
will serve both as a first text in formal logic and an introduction to automation 
issues for students in computer science or mathematics. The book treats 
propositional logic, first-order logic, and first-order logic with equality. In 
each case the initial presentation is semantic, to define the intended subjects 
independently of the choice of proof mechanism. Then many kinds of proof 
procedure are introduced. Results such as completeness, compactness, and 
interpolation are established, and theorem provers are implemented in Prolog. 
This new edition includes material on AE calculus, Herbrand's Theorem, Gentzen's  
Theorem, and related topics.

Reference:  Chin-Liang Chang. Symbolic Logic and Mechanical Theorem Proving. 
Academic Press, 1973.
Short abstract:Mechanical theorem proving is an important subject in 
artificial intelligence. It has been applied to many areas--program analysis, 
program synthesis, deductive question-answering systems, problem-solving systems, 
and robot technology. This classic text provides a thorough discussion of 
mechanical theorem proving and its applications as well as an introduction to 
symbolic logic. A purely model-theoretic approach to first-order logic is 
adopted, and the book emphasizes efficient computer implementations of proof 
techniques. 

Reference: J. Alan Robinson and Andrei Voronkov (eds). Handbook of Automated 
Reasoning. MIT press, 2001. 
Short abstract: Automated reasoning has matured into one of the most 
advanced areas of computer science. It is used in many areas of the field, 
including software and hardware verification, logic and functional programming, 
formal methods, knowledge representation, deductive databases, and artificial 
intelligence. This handbook presents an overview of the fundamental ideas, 
techniques, and methods in automated reasoning and its applications. The material 
covers both theory and implementation. In addition to traditional topics, the 
book covers material that bridges the gap between automated reasoning and related 
areas. Examples include model checking, nonmonotonic reasoning, numerical 
constraints, description logics, and implementation of declarative programming 
languages. 

• • 1.4. A short list of open problems in theories and methods.

First-order logic is a well established formalism, and is the basis for many other subfields such as Description Logics and logic programming.

• 2. TRENDS ON THEORIES AND METHODS, SERVICES AND APPLICATIONS

• • 2.1. Research projects in which contributors are involved, along with a general description. Moreover, suggest for each project the possible future uses and applications related to the Semantic Web, the acceptance and diffusion in each period considered, the benefits, and the problems that will be probably occur.

Name of the project: 
Type: 
Duration: 
Partners: 
Research Institution: 
Industrial Partners: 
Core activities: 
Market opportunities: 
Problems and missing tools: 
Problems – Semantic Web culture is missing: 

Common Logic is an effort to standardize a syntax for (variants of) first-order logic.

The Process Specification Language is an ISO standard language for specifying processes, e.g. Semantic Web services, specified as a set of first-order logic axioms in common logic.

• • 2.2. Some topics that will not be solved in short and medium term, for each of them there is a short explanation of the main reasons and (if possible) some references.

Topics: 
Reason: 
References: none

• 3. TRENDS ON TOOLS
  • 3.1. A list of the most relevant semantic based demos in the area.

The state-of-the-art first-order theorem prover [Vampire http://reliant.teknowledge.com/cgi-bin/cvsweb.cgi/Vampire/] has been used for reasoning with SWRL:

Ian Horrocks, Peter F. Patel-Schneider, Sean Bechhofer, Dmitry Tsarkov: OWL rules: A proposal and prototype implementation. J. Web Sem. 3(1): 23-40 (2005)

Name: Vampire
Website: http://reliant.teknowledge.com/cgi-bin/cvsweb.cgi/Vampire/
Description: see the web page 
References: Alexandre Riazanov, Andrei Voronkov: The design and implementation of 
                  VAMPIRE. AI Commun. 15(2-3): 91-110 (2002)
Main features: State-of-the-art theorem prover
Open problems: Theorem proving with subsets of first-order logic

• • 3.2. A short description of tools that are still missing. A description of business activities and problems they should solve, will be provided.

• 4.Please fell free to add any comment or suggestion.