Related Research Articles
Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic programming language families include Prolog, answer set programming (ASP) and Datalog. In all of these languages, rules are written in the form of clauses:
Prolog is a logic programming language associated with artificial intelligence and computational linguistics.
Constraint programming (CP) is a paradigm for solving combinatorial problems that draws on a wide range of techniques from artificial intelligence, computer science, and operations research. In constraint programming, users declaratively state the constraints on the feasible solutions for a set of decision variables. Constraints differ from the common primitives of imperative programming languages in that they do not specify a step or sequence of steps to execute, but rather the properties of a solution to be found. In addition to constraints, users also need to specify a method to solve these constraints. This typically draws upon standard methods like chronological backtracking and constraint propagation, but may use customized code like a problem-specific branching heuristic.
Constraint satisfaction problems (CSPs) are mathematical questions defined as a set of objects whose state must satisfy a number of constraints or limitations. CSPs represent the entities in a problem as a homogeneous collection of finite constraints over variables, which is solved by constraint satisfaction methods. CSPs are the subject of research in both artificial intelligence and operations research, since the regularity in their formulation provides a common basis to analyze and solve problems of many seemingly unrelated families. CSPs often exhibit high complexity, requiring a combination of heuristics and combinatorial search methods to be solved in a reasonable time. Constraint programming (CP) is the field of research that specifically focuses on tackling these kinds of problems. Additionally, Boolean satisfiability problem (SAT), the satisfiability modulo theories (SMT), mixed integer programming (MIP) and answer set programming (ASP) are all fields of research focusing on the resolution of particular forms of the constraint satisfaction problem.
In artificial intelligence and operations research, constraint satisfaction is the process of finding a solution through a set of constraints that impose conditions that the variables must satisfy. A solution is therefore a set of values for the variables that satisfies all constraints—that is, a point in the feasible region.
Model-based testing is an application of model-based design for designing and optionally also executing artifacts to perform software testing or system testing. Models can be used to represent the desired behavior of a system under test (SUT), or to represent testing strategies and a test environment. The picture on the right depicts the former approach.
Answer set programming (ASP) is a form of declarative programming oriented towards difficult search problems. It is based on the stable model semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers—programs for generating stable models—are used to perform search. The computational process employed in the design of many answer set solvers is an enhancement of the DPLL algorithm and, in principle, it always terminates.
ECLiPSe is a software system for the development and deployment of Constraint Programming applications, e.g. in the areas of optimization, planning, scheduling, resource allocation, timetabling, transport etc. It is also suited for teaching most aspects of combinatorial problem solving, e.g. problem modeling, constraint programming, mathematical programming, and search techniques. It contains constraint solver libraries, a high-level modeling and control language, interfaces to third-party solvers, an integrated development environment and interfaces for embedding into host environments.
CHIP is a constraint logic programming language developed by M. Dincbas, Pascal Van Hentenryck and colleagues in 1985 at the European Computer-Industry Research Centre (ECRC), initially using a Prolog language interface. It was the first programming language to implement Constraint Programming over Finite Domains, and subsequently to introduce the concept of Global Constraints.
In constraint satisfaction, local consistency conditions are properties of constraint satisfaction problems related to the consistency of subsets of variables or constraints. They can be used to reduce the search space and make the problem easier to solve. Various kinds of local consistency conditions are leveraged, including node consistency, arc consistency, and path consistency.
Constraint logic programming is a form of constraint programming, in which logic programming is extended to include concepts from constraint satisfaction. A constraint logic program is a logic program that contains constraints in the body of clauses. An example of a clause including a constraint is A(X,Y):-X+Y>0,B(X),C(Y). In this clause, X+Y>0 is a constraint; A(X,Y), B(X), and C(Y) are literals as in regular logic programming. This clause states one condition under which the statement A(X,Y) holds: X+Y is greater than zero and both B(X) and C(Y) are true.
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.
Concolic testing is a hybrid software verification technique that performs symbolic execution, a classical technique that treats program variables as symbolic variables, along a concrete execution path. Symbolic execution is used in conjunction with an automated theorem prover or constraint solver based on constraint logic programming to generate new concrete inputs with the aim of maximizing code coverage. Its main focus is finding bugs in real-world software, rather than demonstrating program correctness.
Nominal terms are a metalanguage for embedding object languages with binding constructs into. Intuitively, they may be seen as an extension of first-order terms with support for name binding. Consequently, the native notion of equality between two nominal terms is alpha-equivalence. Nominal terms came out of a programme of research into nominal sets, and have a concrete semantics in those sets.
The zebra puzzle is a well-known logic puzzle. Many versions of the puzzle exist, including a version published in Life International magazine on December 17, 1962. The March 25, 1963, issue of Life contained the solution and the names of several hundred successful solvers from around the world.
In information technology a reasoning system is a software system that generates conclusions from available knowledge using logical techniques such as deduction and induction. Reasoning systems play an important role in the implementation of artificial intelligence and knowledge-based systems.
Reachability is a fundamental problem that appears in several different contexts: finite- and infinite-state concurrent systems, computational models like cellular automata and Petri nets, program analysis, discrete and continuous systems, time critical systems, hybrid systems, rewriting systems, probabilistic and parametric systems, and open systems modelled as games.
PROSE was the mathematical 4GL virtual machine that established the holistic modeling paradigm known as Synthetic Calculus. A successor to the SLANG/CUE simulation and optimization language developed at TRW Systems, it was introduced in 1974 on Control Data supercomputers. It was the first commercial language to employ automatic differentiation (AD), which was optimized to loop in the instruction-stack of the CDC 6600 CPU.
In logic, a finite-valued logic is a propositional calculus in which truth values are discrete. Traditionally, in Aristotle's logic, the bivalent logic, also known as binary logic was the norm, as the law of the excluded middle precluded more than two possible values for any proposition. Modern three-valued logic allows for an additional possible truth value.
GOLOG is a high-level logic programming language for the specification and execution of complex actions in dynamical domains. It is based on the situation calculus. It is a first-order logical language for reasoning about action and change. GOLOG was developed at the University of Toronto.
References
- Speeding up constraint propagation. Christian Schulte and Peter J. Stuckey, In Wallace, 2004, pages 619–633.
- Compiling and Executing Declarative Modeling Languages to Gecode [ dead link ]. Raffaele Cipriano, Agostino Dovier, Jacopo Mauro. Conference: International Conference on Logic Programming/Joint International Conference and Symposium on Logic Programming - ICLP(JICSLP), pp. 744–748, 2008
- Monadic Constraint Programming with Gecode. Pieter Wuille, Tom Schrijvers. Proceedings of the 8th International Workshop on Constraint Modelling and Reformulation pages:171-185. International workshop on Constraint Modelling and Reformulation. Lisbon, 20 September 2009.
- A hybrid solver for large neighborhood search: Mixing Gecode and EasyLocal++. Raffaele Cipriano, Luca Di Gaspero, Agostino Dovier. Conference: Hybrid Metaheuristics - HM, pp. 141–155, 2009. DOI: 10.1007/978-3-642-04918-7_11
