Skip to content
/ fol Public

A semantically accurate implementation of first-order logic in JavaScript πŸ‘©β€πŸ«.

Notifications You must be signed in to change notification settings

oelin/fol

Folders and files

NameName
Last commit message
Last commit date

Latest commit

Β 

History

21 Commits
Β 
Β 
Β 
Β 
Β 
Β 

Repository files navigation

FOL

This library provides a semantically accurate implementation of first-order logic (FOL) in JavaScript. It aims to closely replicate the standard set-theoretic formulation of FOL.

Concepts

This library aims to implement all primary concepts found within the standard definition of FOL.

Concept Implementation
First Order Language FirstOrderLanguage(constantSymbols, variableSymbols, functionSymbols, predicateSymbols), FirstOrderParser(firstOrderLanguage)
First Order Structure FirstOrderStructure(firstOrderLanguage, domain, constantsMap, functionsMap, predicatesMap)
Interpretation Function FirstOrderStructure.interpret(symbol)
Domain Of Discourse FirstOrderStructure.domain
Variable Binding FirstOrderAssignment(?variableMap)
Formula Evaluation FirstOrderEvaluator(firstOrderStructure, ?firstOrderAssignment)

Usage

Creating First-Order Models

In this example we create a first-order model for modulo-10 arithmetic.

// The domain of discourse.

const domain = new Set([0, 1, 2, 3, 4, 5, 6, 7, 8, 9])


// Variables.

const variables = ['x', 'y', 'z', 'a', 'b', 'c']


// Mapping between constant symbols and their interpretations.

const constantsMap = {
  0: 0,
  1: 1,
  2: 2,
  3: 3,
  4: 4,
  5: 5,
  6: 6,
  7: 7,
  8: 8,
  9: 9
}


// Mapping between function symbols and their interpretations.

function mod10(n) {
    return ((n % 10) + 10) % 10
}


const functionsMap = {

  // Addition.
  
  F(x, y) {
    return mod10(x + y)
  },
  
  // Subtraction.
  
  G(x, y) {
    return mod10(x - y)
  },
  
  // Successor relation.
  
  S(x) {
    return mod10(x + 1)
  },
  
  // Predecessor
  
  P(x) {
    return mod10(x - 1)
  },
  
  // Additive inverse.
  
  I(x) {
    return mod10(-x)
  }
}


// Mapping between predicates and their interpretations.

const predicatesMap = {

  // Equality in the domain.
  
  M(x, y) {
    return x === y
  },
  
  // Less-than relation.
  
  L(x, y) {
    return x < y
  }
}


// Create the first-order model.

const model = new FirstOrderLogic(
  domain,
  variables,
  constantsMap,
  functionsMap,
  predicatesMap
)

Evaluating Formulae

For all x, there is a y such that y is the successor of x. This should be true.

model.evaluate('AxEyM(y,S(x))') // true

There is no smallest x. This should be false.

model.evaluate('-ExAy(-M(x,y)>L(x,y))') // false

The successor of the predecessor of x is equal to x. This should be true.

model.evaluate('AxM(S(P(x)),x)') // true

The successor of the largest element of the domain is the smallest element of the domain. This should be true.

model.evaluate('ExEy((Az(-M(x,y)>L(x,z))^Az(-M(y,z)>L(z,y)))>M(S(y),x))') // true

There is an element which when summed with its additive inverse, results in 1. This should be false.

model.evaluate('ExM(1,F(x,I(x)))') // false

Any element summed with its additive inverse results in 0. This should be true.

model.evaluate('AxM(0,F(x,I(x)))') // true

There is an element which is its own additive inverse. This should be true, namely on x=0 and x=5.

model.evaluate('ExM(x,I(x))') // true

Efficiency

In this implementation, quantifiers are evaluated by iterating over the domain. Hence, nesting quantifiers leads to nested iteration and therefore a significant increase in evaluation time. If you have three layers of quantification for example, the evaluation time is at worst cubic in the size of the domain.

Future

  • Add support for multicharacter predicate names.
  • Add equality as a primitive binary connective.
  • There's currently working implementations of propositional and modal logic in future.js, however they need to be refactored.

About

A semantically accurate implementation of first-order logic in JavaScript πŸ‘©β€πŸ«.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published